https://github.com/mit-plv/fiat-crypto
Revision 72fe0dddee5e6dceeab0b8a2e6a745abf5287d3e authored by Jason Gross on 15 July 2021, 00:27:45 UTC, committed by Jason Gross on 15 July 2021, 00:28:57 UTC
``` make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync perf-csv ```
1 parent f020c4e
Tip revision: 72fe0dddee5e6dceeab0b8a2e6a745abf5287d3e authored by Jason Gross on 15 July 2021, 00:27:45 UTC
make perf csv
make perf csv
Tip revision: 72fe0dd
time-of-build-general.log
Makefile:111: Skipping bedrock2
/bin/sh: 1: : Permission denied
Makefile:665: src/Rewriter/PerfTesting/Specific/generated/primes.mk: No such file or directory
sed 's/@NATIVE_COMPILER_ARG@/-arg -native-compiler -arg ondemand/g' _CoqProject.in > _CoqProject
COQ_MAKEFILE -f _CoqProject > Makefile.coq
./src/Rewriter/PerfTesting/Specific/make.py primes.txt
Makefile:111: Skipping bedrock2
make --no-print-directory -C rewriter
make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
/home/jgross/.local64/coq/coq-8.11.1/bin/coq_makefile -f _CoqProject -o Makefile.coq
COQDEP VFILES
*** Warning: in file src/Coqprime/num/Lucas.v, library Bignums.DoubleCyclic is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Lucas.v, library Bignums.BigN is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/NEll.v, library Bignums.DoubleCyclic is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/NEll.v, library Bignums.BigN is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleBase is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleSub is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleMul is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleSqrt is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleLift is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleDivn1 is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleDiv is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.DoubleCyclic is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Mod_op.v, library Bignums.BigN is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Pock.v, library Bignums.DoubleCyclic is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/Pock.v, library Bignums.BigN is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/W.v, library Bignums.DoubleCyclic is required and has not been found in the loadpath!
*** Warning: in file src/Coqprime/num/W.v, library Bignums.BigN is required and has not been found in the loadpath!
Makefile:27: Makefile.coq: No such file or directory
echo $COQ_VERSION_INFO (8.11.1) > .coq-version
sed 's/@ML4_OR_MLG@/mlg/g; s/@NATIVE_COMPILER_ARG@/-arg -native-compiler -arg ondemand/g' _CoqProject.in > _CoqProject
COQ_MAKEFILE -f _CoqProject > Makefile.coq
COQ_MAKEFILE -f _CoqProject > Makefile.coq
COQC src/Coqprime/Tactic/Tactic.v
src/Coqprime/Tactic/Tactic (real: 0.06, user: 0.03, sys: 0.02, mem: 58900 ko)
COQC src/Coqprime/N/NatAux.v
src/Coqprime/N/NatAux (real: 0.33, user: 0.22, sys: 0.11, mem: 306528 ko)
COQC src/Coqprime/List/ListAux.v
src/Coqprime/List/ListAux (real: 0.51, user: 0.37, sys: 0.13, mem: 402900 ko)
CP src/Rewriter/Util/plugins/definition_by_tactic.ml{.v811,}
CP src/Rewriter/Util/plugins/RewriterBuildRegistry.v{.v811,}
CP src/Rewriter/Util/plugins/definition_by_tactic.mli{.v811,}
CP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg{.v811,}
CP src/Rewriter/Util/plugins/inductive_from_elim.ml{.v811,}
CP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib{.v811,}
CP src/Rewriter/Util/plugins/inductive_from_elim.mli{.v811,}
CP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg{.v811,}
CP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib{.v811,}
CP src/Rewriter/Util/plugins/rewriter_build.ml{.v811,}
CP src/Rewriter/Util/plugins/rewriter_build.mli{.v811,}
CP src/Rewriter/Util/plugins/rewriter_build_plugin.mlg{.v811,}
CP src/Rewriter/Util/plugins/rewriter_build_plugin.mllib{.v811,}
CP src/Rewriter/Util/plugins/strategy_tactic.ml{.v811,}
CP src/Rewriter/Util/plugins/strategy_tactic.mli{.v811,}
CP src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib{.v811,}
CP src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg{.v811,}
COQPP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg
COQPP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg
COQPP src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg
COQPP src/Rewriter/Util/plugins/rewriter_build_plugin.mlg
CAMLDEP src/Rewriter/Util/plugins/strategy_tactic.mli
CAMLDEP src/Rewriter/Util/plugins/rewriter_build.mli
CAMLDEP src/Rewriter/Util/plugins/inductive_from_elim.mli
CAMLDEP src/Rewriter/Util/plugins/definition_by_tactic.mli
COQDEP src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib
COQDEP src/Rewriter/Util/plugins/rewriter_build_plugin.mllib
COQDEP VFILES
COQDEP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib
CAMLDEP src/Rewriter/Util/plugins/strategy_tactic.ml
COQDEP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib
CAMLDEP src/Rewriter/Util/plugins/rewriter_build.ml
CAMLDEP src/Rewriter/Util/plugins/inductive_from_elim.ml
CAMLDEP src/Rewriter/Util/plugins/definition_by_tactic.ml
CAMLDEP src/Rewriter/Util/plugins/strategy_tactic_plugin.ml
CAMLDEP src/Rewriter/Util/plugins/rewriter_build_plugin.ml
CAMLDEP src/Rewriter/Util/plugins/inductive_from_elim_plugin.ml
CAMLDEP src/Rewriter/Util/plugins/definition_by_tactic_plugin.ml
COQC src/Coqprime/List/Permutation.v
src/Coqprime/List/Permutation (real: 0.57, user: 0.43, sys: 0.13, mem: 404204 ko)
echo $COQ_VERSION_INFO (8.11.1) > .coq-version-short
echo $COQ_VERSION_INFO (8.11.1, April 2020) > .coq-version-short-date
echo $COQ_VERSION_INFO (8.11.1, Apr 4 2020 17:41:20) > .coq-version-compilation-date
echo $COQ_VERSION_INFO (8.11.1, 4.06.1) > .coq-version-ocaml-version
echo $COQ_VERSION_INFO (8.11.1, <ocaml config>) > .coq-version-ocaml-config
echo $COQ_VERSION_INFO (8.11.1, <config>) > .coq-version-config
COQC src/Coqprime/Z/ZCAux.v
src/Coqprime/Z/ZCAux (real: 1.21, user: 1.07, sys: 0.14, mem: 440672 ko)
etc/machine.sh > .machine
etc/machine-extended.sh > .machine-extended
No LSB modules are available.
COQC src/Coqprime/List/Iterator.v
src/Coqprime/List/Iterator (real: 0.45, user: 0.32, sys: 0.12, mem: 404204 ko)
COQC src/Coqprime/List/UList.v
src/Coqprime/List/UList (real: 0.56, user: 0.44, sys: 0.11, mem: 404732 ko)
COQC src/Coqprime/PrimalityTest/FGroup.v
src/Coqprime/PrimalityTest/FGroup (real: 0.38, user: 0.29, sys: 0.09, mem: 373884 ko)
COQC src/Coqprime/List/ZProgression.v
src/Coqprime/List/ZProgression (real: 0.56, user: 0.41, sys: 0.14, mem: 438632 ko)
COQC src/Rewriter/Util/GlobalSettings.v
src/Rewriter/Util/GlobalSettings.vo (real: 0.06, user: 0.01, sys: 0.03, mem: 57028 ko)
COQC src/Rewriter/Util/IffT.v
src/Rewriter/Util/IffT.vo (real: 0.07, user: 0.05, sys: 0.02, mem: 78940 ko)
COQC src/Rewriter/Util/Isomorphism.v
src/Rewriter/Util/Isomorphism.vo (real: 0.05, user: 0.01, sys: 0.03, mem: 58944 ko)
COQC src/Coqprime/PrimalityTest/Root.v
src/Coqprime/PrimalityTest/Root (real: 0.88, user: 0.77, sys: 0.11, mem: 419020 ko)
COQC src/Coqprime/PrimalityTest/IGroup.v
src/Coqprime/PrimalityTest/IGroup (real: 0.53, user: 0.42, sys: 0.10, mem: 414984 ko)
COQC src/Rewriter/Util/HProp.v
src/Rewriter/Util/HProp.vo (real: 0.08, user: 0.05, sys: 0.02, mem: 88592 ko)
COQC src/Rewriter/Util/InductiveHList.v
src/Rewriter/Util/InductiveHList.vo (real: 0.05, user: 0.03, sys: 0.02, mem: 61420 ko)
COQC src/Coqprime/PrimalityTest/Lagrange.v
src/Coqprime/PrimalityTest/Lagrange (real: 0.57, user: 0.46, sys: 0.10, mem: 416128 ko)
COQC src/Rewriter/Util/Tactics/Test.v
src/Rewriter/Util/Tactics/Test.vo (real: 0.06, user: 0.03, sys: 0.02, mem: 57820 ko)
COQC src/Rewriter/Util/Pointed.v
src/Rewriter/Util/Pointed.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 82312 ko)
COQC src/Rewriter/Util/Bool.v
src/Rewriter/Util/Bool.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 134120 ko)
COQC src/Rewriter/Util/Tactics/ConstrFail.v
src/Rewriter/Util/Tactics/ConstrFail.vo (real: 0.05, user: 0.03, sys: 0.02, mem: 58040 ko)
COQC src/Rewriter/Util/Tactics/GetGoal.v
src/Rewriter/Util/Tactics/GetGoal.vo (real: 0.05, user: 0.03, sys: 0.01, mem: 57728 ko)
COQC src/Rewriter/Util/Tactics/Contains.v
src/Rewriter/Util/Tactics/Contains.vo (real: 0.06, user: 0.03, sys: 0.02, mem: 58052 ko)
COQC src/Rewriter/Util/Comparison.v
src/Rewriter/Util/Comparison.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 71736 ko)
COQC src/Rewriter/Util/Tactics/DebugPrint.v
src/Rewriter/Util/Tactics/DebugPrint.vo (real: 0.06, user: 0.05, sys: 0.00, mem: 65696 ko)
COQC src/Rewriter/Util/TypeList.v
src/Rewriter/Util/TypeList.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 59852 ko)
COQC src/Rewriter/Util/Tactics/PrintContext.v
src/Rewriter/Util/Tactics/PrintContext.vo (real: 0.05, user: 0.02, sys: 0.02, mem: 58128 ko)
COQC src/Rewriter/Util/Tactics/TransparentAssert.v
src/Rewriter/Util/Tactics/TransparentAssert.vo (real: 0.05, user: 0.03, sys: 0.01, mem: 58620 ko)
COQC src/Rewriter/Util/Tactics/EvarNormalize.v
src/Rewriter/Util/Tactics/EvarNormalize.vo (real: 0.05, user: 0.04, sys: 0.01, mem: 57892 ko)
COQC src/Rewriter/Util/Tactics/CPSId.v
src/Rewriter/Util/Tactics/CPSId.vo (real: 0.05, user: 0.03, sys: 0.02, mem: 60264 ko)
COQC src/Rewriter/Util/Bool/Equality.v
src/Rewriter/Util/Bool/Equality.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 68676 ko)
COQC src/Rewriter/Util/Sigma/Related.v
src/Rewriter/Util/Sigma/Related.vo (real: 0.10, user: 0.07, sys: 0.03, mem: 112776 ko)
COQC src/Rewriter/Util/Tactics/SetEvars.v
src/Rewriter/Util/Tactics/SetEvars.vo (real: 0.05, user: 0.03, sys: 0.01, mem: 57764 ko)
CAMLC -c src/Rewriter/Util/plugins/strategy_tactic.mli
CAMLC -c src/Rewriter/Util/plugins/definition_by_tactic.mli
CAMLC -c src/Rewriter/Util/plugins/inductive_from_elim.mli
COQC src/Rewriter/Util/Tactics/SubstEvars.v
src/Rewriter/Util/Tactics/SubstEvars.vo (real: 0.05, user: 0.01, sys: 0.03, mem: 57620 ko)
CAMLC -c src/Rewriter/Util/plugins/rewriter_build.mli
COQC src/Coqprime/Z/ZSum.v
src/Coqprime/Z/ZSum (real: 0.97, user: 0.86, sys: 0.10, mem: 442288 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo (real: 0.15, user: 0.13, sys: 0.02, mem: 172084 ko)
COQC src/Rewriter/Util/Strings/Decimal.v
src/Rewriter/Util/Strings/Decimal.vo (real: 0.34, user: 0.27, sys: 0.06, mem: 299788 ko)
COQC src/Rewriter/Util/FixCoqMistakes.v
src/Rewriter/Util/FixCoqMistakes.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 71976 ko)
COQC src/Rewriter/Util/Equality.v
src/Rewriter/Util/Equality.vo (real: 0.14, user: 0.11, sys: 0.03, mem: 140384 ko)
COQC src/Rewriter/Util/Tactics/Head.v
src/Rewriter/Util/Tactics/Head.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 65196 ko)
COQC src/Rewriter/Util/Tactics/DestructHyps.v
src/Rewriter/Util/Tactics/DestructHyps.vo (real: 0.06, user: 0.05, sys: 0.01, mem: 67296 ko)
COQC src/Rewriter/Util/Tactics/SpecializeBy.v
src/Rewriter/Util/Tactics/SpecializeBy.vo (real: 0.06, user: 0.02, sys: 0.03, mem: 66184 ko)
COQC src/Coqprime/PrimalityTest/Euler.v
src/Coqprime/PrimalityTest/Euler (real: 0.60, user: 0.47, sys: 0.12, mem: 439784 ko)
COQC src/Rewriter/Util/Tactics/Not.v
src/Rewriter/Util/Tactics/Not.vo (real: 0.05, user: 0.04, sys: 0.01, mem: 58024 ko)
COQC src/Rewriter/Util/Tactics/SplitInContext.v
src/Rewriter/Util/Tactics/SplitInContext.vo (real: 0.06, user: 0.03, sys: 0.02, mem: 66520 ko)
COQC src/Rewriter/Util/Tactics/SetoidSubst.v
src/Rewriter/Util/Tactics/SetoidSubst.vo (real: 0.05, user: 0.02, sys: 0.03, mem: 59268 ko)
COQC src/Rewriter/Util/Tactics/RunTacticAsConstr.v
src/Rewriter/Util/Tactics/RunTacticAsConstr.vo (real: 0.07, user: 0.05, sys: 0.01, mem: 65444 ko)
COQC src/Rewriter/Util/Tactics/UniquePose.v
src/Rewriter/Util/Tactics/UniquePose.vo (real: 0.06, user: 0.03, sys: 0.02, mem: 65848 ko)
COQC src/Coqprime/PrimalityTest/EGroup.v
src/Coqprime/PrimalityTest/EGroup (real: 1.45, user: 1.32, sys: 0.12, mem: 447016 ko)
COQC src/Rewriter/Util/Tactics/HeadUnderBinders.v
src/Rewriter/Util/Tactics/HeadUnderBinders.vo (real: 0.06, user: 0.03, sys: 0.03, mem: 65400 ko)
COQC src/Rewriter/Util/Tactics/PrintGoal.v
src/Rewriter/Util/Tactics/PrintGoal.vo (real: 0.05, user: 0.02, sys: 0.03, mem: 57996 ko)
COQC src/Rewriter/Util/Tactics/CacheTerm.v
src/Rewriter/Util/Tactics/CacheTerm.vo (real: 0.06, user: 0.04, sys: 0.01, mem: 61020 ko)
COQC src/Rewriter/Util/Logic/ProdForall.v
src/Rewriter/Util/Logic/ProdForall.vo (real: 0.07, user: 0.05, sys: 0.02, mem: 78960 ko)
CAMLOPT -c src/Rewriter/Util/plugins/strategy_tactic.ml
COQC src/Rewriter/Util/Tactics/WarnIfGoalsRemain.v
src/Rewriter/Util/Tactics/WarnIfGoalsRemain.vo (real: 0.05, user: 0.03, sys: 0.02, mem: 57988 ko)
CAMLOPT -c src/Rewriter/Util/plugins/definition_by_tactic.ml
CAMLOPT -c src/Rewriter/Util/plugins/inductive_from_elim.ml
File "src/Rewriter/Util/plugins/inductive_from_elim.ml", line 67, characters 6-61:
Warning 3: deprecated: ComInductive.declare_mutual_inductive_with_eliminations
Please use DeclareInd.declare_mutual_inductive_with_eliminations
CAMLOPT -c src/Rewriter/Util/plugins/definition_by_tactic_plugin.ml
COQC src/Rewriter/Util/Tactics/AssertSucceedsPreserveError.v
src/Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 65168 ko)
CAMLOPT -c src/Rewriter/Util/plugins/inductive_from_elim_plugin.ml
COQC src/Rewriter/Util/Notations.v
src/Rewriter/Util/Notations.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 78268 ko)
COQC src/Rewriter/Util/NatUtil.v
src/Rewriter/Util/NatUtil.vo (real: 1.93, user: 1.77, sys: 0.16, mem: 456796 ko)
COQC src/Rewriter/Util/PrimitiveProd.v
src/Rewriter/Util/PrimitiveProd.vo (real: 0.17, user: 0.10, sys: 0.07, mem: 192512 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
src/Rewriter/Rewriter/Examples/PerfTesting/Harness.vo (real: 1.50, user: 1.38, sys: 0.12, mem: 449344 ko)
COQC src/Rewriter/Util/Tactics/BreakMatch.v
src/Rewriter/Util/Tactics/BreakMatch.vo (real: 0.07, user: 0.05, sys: 0.02, mem: 69416 ko)
COQC src/Rewriter/Util/Prod.v
src/Rewriter/Util/Prod.vo (real: 0.22, user: 0.14, sys: 0.08, mem: 259760 ko)
COQC src/Rewriter/Util/Sigma.v
src/Rewriter/Util/Sigma.vo (real: 0.22, user: 0.14, sys: 0.07, mem: 235636 ko)
COQC src/Rewriter/Util/Tactics/DestructHead.v
src/Rewriter/Util/Tactics/DestructHead.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 73740 ko)
COQC src/Rewriter/Util/Tactics/DoWithHyp.v
src/Rewriter/Util/Tactics/DoWithHyp.vo (real: 0.06, user: 0.03, sys: 0.02, mem: 65544 ko)
COQC src/Rewriter/Util/LetIn.v
src/Rewriter/Util/LetIn.vo (real: 0.09, user: 0.03, sys: 0.05, mem: 94276 ko)
COQC src/Rewriter/Util/CPSNotations.v
src/Rewriter/Util/CPSNotations.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 72592 ko)
COQC src/Rewriter/Util/Tactics/SpecializeAllWays.v
src/Rewriter/Util/Tactics/SpecializeAllWays.vo (real: 0.06, user: 0.04, sys: 0.01, mem: 65440 ko)
CAMLOPT -c src/Rewriter/Util/plugins/strategy_tactic_plugin.ml
CAMLOPT -c src/Rewriter/Util/plugins/rewriter_build.ml
COQC src/Rewriter/Util/Logic/ExistsEqAnd.v
src/Rewriter/Util/Logic/ExistsEqAnd.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 96444 ko)
COQC src/Rewriter/Util/PrimitiveSigma.v
src/Rewriter/Util/PrimitiveSigma.vo (real: 0.16, user: 0.11, sys: 0.04, mem: 160276 ko)
CAMLOPT -a -o src/Rewriter/Util/plugins/definition_by_tactic_plugin.cmxa
CAMLOPT -a -o src/Rewriter/Util/plugins/inductive_from_elim_plugin.cmxa
COQC src/Rewriter/Util/PrimitiveHList.v
src/Rewriter/Util/PrimitiveHList.vo (real: 0.15, user: 0.09, sys: 0.05, mem: 152024 ko)
COQC src/Coqprime/PrimalityTest/Cyclic.v
src/Coqprime/PrimalityTest/Cyclic (real: 0.92, user: 0.80, sys: 0.12, mem: 445216 ko)
COQC src/Rewriter/Util/Strings/Ascii.v
src/Rewriter/Util/Strings/Ascii.vo (real: 0.29, user: 0.21, sys: 0.08, mem: 273076 ko)
COQC src/Rewriter/Util/Tactics/RewriteHyp.v
src/Rewriter/Util/Tactics/RewriteHyp.vo (real: 0.07, user: 0.07, sys: 0.00, mem: 84972 ko)
CAMLOPT -a -o src/Rewriter/Util/plugins/strategy_tactic_plugin.cmxa
CAMLOPT -c src/Rewriter/Util/plugins/rewriter_build_plugin.ml
COQC src/Rewriter/Util/Option.v
src/Rewriter/Util/Option.vo (real: 0.38, user: 0.32, sys: 0.06, mem: 312496 ko)
CAMLOPT -shared -o src/Rewriter/Util/plugins/definition_by_tactic_plugin.cmxs
CAMLOPT -shared -o src/Rewriter/Util/plugins/inductive_from_elim_plugin.cmxs
COQC src/Rewriter/Util/Decidable.v
src/Rewriter/Util/Decidable.vo (real: 0.66, user: 0.52, sys: 0.13, mem: 397296 ko)
COQC src/Rewriter/Language/PreCommon.v
src/Rewriter/Language/PreCommon.vo (real: 0.15, user: 0.10, sys: 0.04, mem: 154728 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
src/Rewriter/Rewriter/Examples/PerfTesting/Sample.vo (real: 0.95, user: 0.75, sys: 0.19, mem: 448392 ko)
COQC src/Rewriter/Util/Strings/String.v
src/Rewriter/Util/Strings/String.vo (real: 0.55, user: 0.42, sys: 0.12, mem: 436804 ko)
COQC src/Coqprime/PrimalityTest/Zp.v
src/Coqprime/PrimalityTest/Zp (real: 0.80, user: 0.65, sys: 0.15, mem: 445568 ko)
COQC src/Rewriter/Util/OptionList.v
src/Rewriter/Util/OptionList.vo (real: 0.29, user: 0.21, sys: 0.07, mem: 340408 ko)
COQC src/Rewriter/Util/ListUtil/SetoidList.v
src/Rewriter/Util/ListUtil/SetoidList.vo (real: 0.19, user: 0.11, sys: 0.07, mem: 203680 ko)
CAMLOPT -shared -o src/Rewriter/Util/plugins/strategy_tactic_plugin.cmxs
CAMLOPT -a -o src/Rewriter/Util/plugins/rewriter_build_plugin.cmxa
COQC src/Rewriter/Util/FMapPositive/Equality.v
src/Rewriter/Util/FMapPositive/Equality.vo (real: 0.38, user: 0.26, sys: 0.11, mem: 367084 ko)
COQC src/Rewriter/Util/Sum.v
src/Rewriter/Util/Sum.vo (real: 0.58, user: 0.46, sys: 0.12, mem: 397100 ko)
COQC src/Rewriter/Util/MSetPositive/Equality.v
src/Rewriter/Util/MSetPositive/Equality.vo (real: 0.49, user: 0.36, sys: 0.13, mem: 426216 ko)
COQC src/Rewriter/Language/Pre.v
src/Rewriter/Language/Pre.vo (real: 0.16, user: 0.10, sys: 0.05, mem: 160356 ko)
COQC src/Rewriter/Util/plugins/StrategyTactic.v
src/Rewriter/Util/plugins/StrategyTactic.vo (real: 0.05, user: 0.01, sys: 0.03, mem: 57968 ko)
COQC src/Rewriter/Util/Strings/Parse/Common.v
src/Rewriter/Util/Strings/Parse/Common.vo (real: 0.40, user: 0.30, sys: 0.09, mem: 347368 ko)
CAMLOPT -shared -o src/Rewriter/Util/plugins/rewriter_build_plugin.cmxs
COQC src/Rewriter/Util/MSetPositive/Facts.v
src/Rewriter/Util/MSetPositive/Facts.vo (real: 0.57, user: 0.45, sys: 0.12, mem: 448808 ko)
COQC src/Rewriter/Util/Strings/ParseArithmetic.v
src/Rewriter/Util/Strings/ParseArithmetic.vo (real: 0.60, user: 0.49, sys: 0.11, mem: 447844 ko)
COQC src/Rewriter/Util/ListUtil/Forall.v
src/Rewriter/Util/ListUtil/Forall.vo (real: 1.32, user: 1.17, sys: 0.14, mem: 443628 ko)
COQC src/Rewriter/Util/ListUtil.v
src/Rewriter/Util/ListUtil.vo (real: 7.96, user: 7.78, sys: 0.18, mem: 509412 ko)
COQC src/Rewriter/Language/PreLemmas.v
src/Rewriter/Language/PreLemmas.vo (real: 0.46, user: 0.30, sys: 0.15, mem: 403932 ko)
COQC src/Rewriter/Util/Bool/Reflect.v
src/Rewriter/Util/Bool/Reflect.vo (real: 1.71, user: 1.60, sys: 0.10, mem: 466444 ko)
COQC src/Rewriter/Language/Language.v
src/Rewriter/Language/Language.vo (real: 1.39, user: 1.23, sys: 0.16, mem: 481708 ko)
COQC src/Rewriter/Language/UnderLets.v
src/Rewriter/Language/UnderLets.vo (real: 0.63, user: 0.48, sys: 0.14, mem: 468940 ko)
COQC src/Rewriter/Language/Inversion.v
src/Rewriter/Language/Inversion.vo (real: 23.07, user: 22.83, sys: 0.20, mem: 637788 ko)
COQC src/Rewriter/Language/IdentifiersBasicLibrary.v
src/Rewriter/Language/IdentifiersBasicLibrary.vo (real: 4.72, user: 4.56, sys: 0.14, mem: 529044 ko)
COQC src/Rewriter/Language/IdentifiersBasicGenerate.v
src/Rewriter/Language/IdentifiersBasicGenerate.vo (real: 0.73, user: 0.60, sys: 0.13, mem: 475788 ko)
COQC src/Rewriter/Language/IdentifiersLibrary.v
src/Rewriter/Language/IdentifiersLibrary.vo (real: 1.77, user: 1.61, sys: 0.15, mem: 522616 ko)
COQC src/Rewriter/Language/IdentifiersGenerate.v
src/Rewriter/Language/IdentifiersGenerate.vo (real: 1.05, user: 0.91, sys: 0.13, mem: 508488 ko)
COQC src/Rewriter/Rewriter/Rewriter.v
src/Rewriter/Rewriter/Rewriter.vo (real: 1.57, user: 1.40, sys: 0.17, mem: 520508 ko)
COQC src/Rewriter/Rewriter/Reify.v
src/Rewriter/Rewriter/Reify.vo (real: 1.44, user: 1.26, sys: 0.17, mem: 519576 ko)
COQC src/Rewriter/Language/IdentifiersLibraryProofs.v
Finished transaction in 2.212 secs (2.212u,0.s) (successful)
Finished transaction in 0.746 secs (0.746u,0.s) (successful)
Finished transaction in 0.093 secs (0.093u,0.s) (successful)
Finished transaction in 1.428 secs (1.424u,0.003s) (successful)
src/Rewriter/Language/IdentifiersLibraryProofs.vo (real: 12.95, user: 12.73, sys: 0.21, mem: 633032 ko)
COQC src/Rewriter/Language/IdentifiersGenerateProofs.v
src/Rewriter/Language/IdentifiersGenerateProofs.vo (real: 0.99, user: 0.83, sys: 0.16, mem: 508464 ko)
COQC src/Rewriter/Language/Wf.v
Finished transaction in 4.368 secs (4.352u,0.016s) (successful)
Finished transaction in 3.44 secs (3.432u,0.007s) (successful)
src/Rewriter/Language/Wf.vo (real: 31.36, user: 31.14, sys: 0.22, mem: 758704 ko)
COQC src/Rewriter/Language/UnderLetsProofs.v
src/Rewriter/Language/UnderLetsProofs.vo (real: 77.19, user: 76.92, sys: 0.25, mem: 865976 ko)
COQC src/Rewriter/Rewriter/ProofsCommon.v
src/Rewriter/Rewriter/ProofsCommon.vo (real: 57.09, user: 56.82, sys: 0.27, mem: 874064 ko)
COQC src/Rewriter/Rewriter/ProofsCommonTactics.v
src/Rewriter/Rewriter/ProofsCommonTactics.vo (real: 1.15, user: 0.99, sys: 0.16, mem: 523948 ko)
COQC src/Rewriter/Rewriter/InterpProofs.v
src/Rewriter/Rewriter/InterpProofs.vo (real: 64.61, user: 64.22, sys: 0.31, mem: 956596 ko)
COQC src/Rewriter/Rewriter/Wf.v
Finished transaction in 27.209 secs (27.201u,0.007s) (successful)
src/Rewriter/Rewriter/Wf.vo (real: 117.40, user: 117.12, sys: 0.27, mem: 958760 ko)
COQC src/Rewriter/Rewriter/AllTactics.v
src/Rewriter/Rewriter/AllTactics.vo (real: 1.33, user: 1.16, sys: 0.16, mem: 539956 ko)
COQC src/Rewriter/Util/plugins/RewriterBuildRegistryImports.v
src/Rewriter/Util/plugins/RewriterBuildRegistryImports.vo (real: 0.99, user: 0.78, sys: 0.21, mem: 529540 ko)
COQC src/Rewriter/Util/plugins/RewriterBuildRegistry.v
src/Rewriter/Util/plugins/RewriterBuildRegistry.vo (real: 0.98, user: 0.81, sys: 0.17, mem: 531088 ko)
COQC src/Rewriter/Util/plugins/RewriterBuild.v
src/Rewriter/Util/plugins/RewriterBuild.vo (real: 0.98, user: 0.86, sys: 0.12, mem: 531716 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/Settings.v
File "./src/Rewriter/Rewriter/Examples/PerfTesting/Settings.v", line 10, characters 0-32:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
src/Rewriter/Rewriter/Examples/PerfTesting/Settings.vo (real: 0.99, user: 0.90, sys: 0.09, mem: 534468 ko)
COQC src/Rewriter/Demo.v
OrdersEx.Nat_as_OT.add_0_r: forall n : nat, n + 0 = n
OrdersEx.Nat_as_DT.add_0_r: forall n : nat, n + 0 = n
Nat.add_0_r: forall n : nat, n + 0 = n
NPeano.Nat.add_0_r: forall n : nat, n + 0 = n
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.297 secs (0.297u,0.s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.19 secs (0.19u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.012 secs (0.012u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.067 secs (0.067u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.674 secs (0.674u,0.s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.153 secs (1.15u,0.003s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.015 secs (0.015u,0.s) (success)
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
Tactic call ran for 0.029 secs (0.029u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.015 secs (0.011u,0.003s) (success)
Tactic call ran for 0.098 secs (0.098u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.129 secs (0.129u,0.s) (success)
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Demo.vo (real: 14.57, user: 14.33, sys: 0.23, mem: 745468 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.303 secs (0.302u,0.s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.203 secs (0.203u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.013 secs (0.013u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.073 secs (0.073u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.719 secs (0.71u,0.007s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.133 secs (1.132u,0.s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.088 secs (0.088u,0.s) (success)
Tactic call ran for 0.024 secs (0.024u,0.s) (success)
Tactic call ran for 0.072 secs (0.072u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.03 secs (0.03u,0.s) (success)
Tactic call ran for 0.46 secs (0.456u,0.003s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.41 secs (0.41u,0.s) (success)
Tactic call ran for 0.167 secs (0.167u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
Finished transaction in 14.749 secs (14.684u,0.047s) (successful)
File "./src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v", line 342, characters 0-31:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
Profiling to file ./native_compute_profile_e4e655.data
Finished transaction in 8.399 secs (2.936u,0.087s) (successful)
File "./src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v", line 460, characters 0-32:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo (real: 25.04, user: 24.44, sys: 0.56, mem: 765688 ko)
COQC src/Rewriter/Rewriter/Examples/PrefixSums.v
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.366 secs (0.366u,0.s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.226 secs (0.226u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.025 secs (0.025u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.074 secs (0.074u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.773 secs (0.773u,0.s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.268 secs (1.264u,0.003s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.308 secs (0.304u,0.003s) (success)
Tactic call ran for 0.919 secs (0.907u,0.011s) (success)
Tactic call ran for 0.19 secs (0.186u,0.003s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.238 secs (0.238u,0.s) (success)
Tactic call ran for 1.943 secs (1.943u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 2.182 secs (2.182u,0.s) (success)
Tactic call ran for 1.487 secs (1.487u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Rewriter/Examples/PrefixSums.vo (real: 33.09, user: 32.89, sys: 0.19, mem: 812220 ko)
COQC src/Rewriter/Rewriter/Examples.v
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.285 secs (0.281u,0.004s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.175 secs (0.175u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.015 secs (0.015u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.065 secs (0.065u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.656 secs (0.656u,0.s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.143 secs (1.139u,0.003s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.005 secs (0.005u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Tactic call ran for 0.031 secs (0.031u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.009 secs (0.009u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.049 secs (0.049u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
Finished transaction in 10.558 secs (10.526u,0.032s) (successful)
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.359 secs (0.359u,0.s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.232 secs (0.232u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.018 secs (0.018u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.078 secs (0.078u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.777 secs (0.777u,0.s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.33 secs (1.326u,0.003s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.179 secs (0.179u,0.s) (success)
Tactic call ran for 0.144 secs (0.144u,0.s) (success)
Tactic call ran for 0.117 secs (0.117u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.072 secs (0.072u,0.s) (success)
Tactic call ran for 1.205 secs (1.205u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 1.144 secs (1.144u,0.s) (success)
Tactic call ran for 0.687 secs (0.687u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
Finished transaction in 22.362 secs (22.345u,0.015s) (successful)
Success: (dlet y0 : Z := e1 + e2 in
[y; y + 1; y + 2; y + y0; y + (y0 + 1)])
Success: [x1; x1; x1; x2; x2; x2; x3; x3; x3]
src/Rewriter/Rewriter/Examples.vo (real: 35.39, user: 35.19, sys: 0.20, mem: 811208 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.296 secs (0.296u,0.s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.198 secs (0.198u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.013 secs (0.013u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.073 secs (0.073u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.677 secs (0.669u,0.007s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.089 secs (1.085u,0.003s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.084 secs (0.084u,0.s) (success)
Tactic call ran for 0.019 secs (0.019u,0.s) (success)
Tactic call ran for 0.072 secs (0.072u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.023 secs (0.023u,0.s) (success)
Tactic call ran for 0.453 secs (0.453u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.357 secs (0.357u,0.s) (success)
Tactic call ran for 0.151 secs (0.151u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
Finished transaction in 14.175 secs (14.123u,0.051s) (successful)
File "./src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v", line 139, characters 0-31:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
Profiling to file ./native_compute_profile_4983c7.data
Finished transaction in 1.3 secs (0.689u,0.084s) (successful)
src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo (real: 16.95, user: 16.55, sys: 0.38, mem: 695192 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.303 secs (0.299u,0.003s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.198 secs (0.194u,0.003s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.012 secs (0.012u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.071 secs (0.071u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.734 secs (0.73u,0.004s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.167 secs (1.163u,0.003s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.192 secs (0.192u,0.s) (success)
Tactic call ran for 0.084 secs (0.084u,0.s) (success)
Tactic call ran for 0.135 secs (0.135u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.06 secs (0.06u,0.s) (success)
Tactic call ran for 1.031 secs (1.031u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.876 secs (0.876u,0.s) (success)
Tactic call ran for 0.539 secs (0.527u,0.011s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
Finished transaction in 19.118 secs (19.058u,0.059s) (successful)
File "./src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v", line 234, characters 0-31:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
Profiling to file ./native_compute_profile_4d5a03.data
Finished transaction in 31.114 secs (27.623u,0.167s) (successful)
File "./src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v", line 384, characters 0-32:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo (real: 52.02, user: 51.43, sys: 0.57, mem: 806092 ko)
COQC src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Proving is_simple_correct0...
Tactic call ran for 0.467 secs (0.463u,0.003s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.265 secs (0.265u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.056 secs (0.056u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.089 secs (0.089u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 0.841 secs (0.841u,0.s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0.001 secs (0.u,0.001s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 1.386 secs (1.385u,0.001s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.383 secs (0.379u,0.004s) (success)
Tactic call ran for 2.698 secs (2.678u,0.019s) (success)
Tactic call ran for 0.187 secs (0.187u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.268 secs (0.264u,0.003s) (success)
Tactic call ran for 1.783 secs (1.779u,0.004s) (success)
Proving Rewriter_Interp...
Tactic call ran for 2.309 secs (2.309u,0.s) (success)
Tactic call ran for 1.017 secs (1.017u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
Finished transaction in 38.989 secs (38.877u,0.111s) (successful)
File "./src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v", line 198, characters 0-31:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
Profiling to file ./native_compute_profile_31e63f.data
Finished transaction in 1.761 secs (1.1u,0.092s) (successful)
File "./src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v", line 283, characters 0-32:
Warning: There is no option NativeCompute Timing. [unknown-option,option]
src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo (real: 42.43, user: 41.97, sys: 0.44, mem: 965052 ko)
COQDEP VFILES
*** Warning: in file src/Algebra/NsatzTactic.v, declared ML module nsatz_plugin has not been found!
*** Warning: in file src/Bedrock/Field/Common/Tactics.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Tactics.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Tactics.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Tactics.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library bedrock2.WeakestPrecondition is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Types.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library bedrock2.WeakestPrecondition is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library coqutil.Tactics.destr is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Util.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/ByteBounds.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/ByteBounds.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/ByteBounds.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/ByteBounds.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/ByteBounds.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MaxBounds.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MaxBounds.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MaxBounds.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Arrays/MaxBounds.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Names/MakeNames.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Common/Names/MakeNames.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Interface/Compilation.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Interface/Representation.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Interface/Representation.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Interface/Representation.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Stringification/Stringification.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Stringification/Stringification.v, library bedrock2.ToCString is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Stringification/Stringification.v, library bedrock2.BasicC64Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/EncodeDecode.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/LadderStep.v, library bedrock2.NotationsCustomEntry is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/MulTwice.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/MulTwice.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/MulTwice.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/MulTwice.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/MulTwice.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/MulTwice.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Examples/MulTwice.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Bignum.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Bignum.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Bignum.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Bignum.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Bignum.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Bignum.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Bignum.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Operation.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library bedrock2.WeakestPrecondition is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/Tactics.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.WeakestPrecondition is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.WeakestPrecondition is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/ComputedOp.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library Rupicola.Lib.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/Signature.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/ReifiedOperation.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/Tactics.v, library bedrock2.WeakestPrecondition is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/Tactics.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/Tactics.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/Tactics.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/Tactics.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Expr.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Flatten.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Flatten.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Flatten.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Func.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Func.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Func.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/LoadStoreList.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/LoadStoreList.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/LoadStoreList.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/LoadStoreList.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/LoadStoreList.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults32.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults32.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults32.v, library bedrock2.BasicC32Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults64.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults64.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Parameters/Defaults64.v, library bedrock2.BasicC64Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Cmd.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Equivalence.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Equivalence.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Equivalence.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Equivalence.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Equivalence.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Equivalence.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Expr.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Expr.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Expr.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Expr.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Expr.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Flatten.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/Func.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library bedrock2.Array is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library bedrock2.Scalars is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library bedrock2.ProgramLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library bedrock2.WeakestPreconditionProperties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library coqutil.Datatypes.List is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/LoadStoreList.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library bedrock2.Map.Separation is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library bedrock2.Map.SeparationLogic is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library coqutil.Map.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/UsedVarnames.v, library coqutil.Datatypes.PropSet is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v, library bedrock2.Syntax is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v, library coqutil.Word.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v, library coqutil.Word.Properties is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v, library coqutil.Map.Interface is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/Loops.v, library Rupicola.Lib.ControlFlow.DownTo is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/Point.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/LadderStep.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/MontgomeryEquivalence.v, library Rupicola.Lib.ControlFlow.CondSwap is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/MontgomeryEquivalence.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/MontgomeryEquivalence.v, library coqutil.Tactics.Tactics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/MontgomeryLadder.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/MontgomeryLadder.v, library Rupicola.Lib.SepLocals is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/MontgomeryLadder.v, library Rupicola.Lib.ControlFlow.CondSwap is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/MontgomeryLadder.v, library Rupicola.Lib.ControlFlow.DownTo is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/ScalarMult.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Group/ScalarMult/ScalarMult.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/ScalarField/Interface/Compilation.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Specs/Field.v, library coqutil.Byte is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Specs/Field.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Specs/Group.v, library bedrock2.Semantics is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Specs/Group.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
*** Warning: in file src/Bedrock/Specs/ScalarField.v, library Rupicola.Lib.Api is required and has not been found in the loadpath!
Makefile:111: Skipping bedrock2
make --no-print-directory -C rewriter
make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date.
echo $COQ_VERSION_INFO (8.11.1) > .coq-version-short
echo $COQ_VERSION_INFO (8.11.1, April 2020) > .coq-version-short-date
echo $COQ_VERSION_INFO (8.11.1, Apr 4 2020 17:41:20) > .coq-version-compilation-date
echo $COQ_VERSION_INFO (8.11.1, 4.06.1) > .coq-version-ocaml-version
echo $COQ_VERSION_INFO (8.11.1, <ocaml config>) > .coq-version-ocaml-config
echo $COQ_VERSION_INFO (8.11.1, <config>) > .coq-version-config
etc/machine.sh > .machine
etc/machine-extended.sh > .machine-extended
No LSB modules are available.
make[2]: Nothing to be done for 'real-all'.
COQC src/Util/GlobalSettings.v
src/Util/GlobalSettings.vo (real: 0.07, user: 0.05, sys: 0.02, mem: 62580 ko)
COQC src/Util/Isomorphism.v
src/Util/Isomorphism.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 64452 ko)
COQC src/Util/IffT.v
src/Util/IffT.vo (real: 0.09, user: 0.05, sys: 0.04, mem: 84056 ko)
COQC src/Util/HProp.v
src/Util/HProp.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 93952 ko)
COQC src/Util/Tactics/Test.v
src/Util/Tactics/Test.vo (real: 0.07, user: 0.03, sys: 0.04, mem: 62820 ko)
COQC src/Util/Tactics/ConstrFail.v
src/Util/Tactics/ConstrFail.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 63168 ko)
COQC src/Util/Pointed.v
src/Util/Pointed.vo (real: 0.10, user: 0.04, sys: 0.05, mem: 87468 ko)
COQC src/Util/Tactics/Contains.v
src/Util/Tactics/Contains.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 63204 ko)
COQC src/Util/Comparison.v
src/Util/Comparison.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 77168 ko)
COQC src/Util/Tactics/GetGoal.v
src/Util/Tactics/GetGoal.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 62924 ko)
COQC src/Util/Tactics/DebugPrint.v
src/Util/Tactics/DebugPrint.vo (real: 0.08, user: 0.05, sys: 0.03, mem: 70668 ko)
COQC src/Util/Structures/Orders.v
src/Util/Structures/Orders.vo (real: 0.10, user: 0.07, sys: 0.03, mem: 91364 ko)
COQC src/Util/Bool/Equality.v
src/Util/Bool/Equality.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 73660 ko)
COQC src/Util/Tactics/HasBody.v
src/Util/Tactics/HasBody.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 62820 ko)
COQC src/Util/ListUtil/NthExt.v
src/Util/ListUtil/NthExt.vo (real: 0.30, user: 0.19, sys: 0.10, mem: 269772 ko)
COQC src/Util/Strings/Decimal.v
src/Util/Strings/Decimal.vo (real: 0.36, user: 0.25, sys: 0.11, mem: 304756 ko)
COQC src/Util/ZUtil/Tactics/CompareToSgn.v
src/Util/ZUtil/Tactics/CompareToSgn.vo (real: 0.33, user: 0.24, sys: 0.08, mem: 290120 ko)
COQC src/Util/ZUtil/Hints/Core.v
src/Util/ZUtil/Hints/Core.vo (real: 0.41, user: 0.31, sys: 0.09, mem: 343916 ko)
COQC src/Util/ZUtil/Tactics/DivideExistsMul.v
src/Util/ZUtil/Tactics/DivideExistsMul.vo (real: 0.41, user: 0.28, sys: 0.12, mem: 339108 ko)
COQC src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
src/Util/ZUtil/Tactics/ReplaceNegWithPos.vo (real: 0.42, user: 0.30, sys: 0.11, mem: 345840 ko)
COQC src/Util/ZUtil/Odd.v
src/Util/ZUtil/Odd.vo (real: 0.42, user: 0.31, sys: 0.11, mem: 372036 ko)
COQC src/Util/Tactics/OnSubterms.v
src/Util/Tactics/OnSubterms.vo (real: 0.06, user: 0.03, sys: 0.02, mem: 63056 ko)
COQC src/Util/ZUtil/Tactics/PrimeBound.v
src/Util/ZUtil/Tactics/PrimeBound.vo (real: 0.36, user: 0.24, sys: 0.11, mem: 304528 ko)
COQC src/Util/Tactics/Revert.v
src/Util/Tactics/Revert.vo (real: 0.06, user: 0.04, sys: 0.01, mem: 62988 ko)
COQC src/Algebra/NsatzTactic.v
src/Algebra/NsatzTactic.vo (real: 1.07, user: 0.93, sys: 0.13, mem: 447144 ko)
COQC src/Util/Decidable/Bool2Prop.v
src/Util/Decidable/Bool2Prop.vo (real: 0.28, user: 0.20, sys: 0.08, mem: 262900 ko)
COQC src/Util/Factorize.v
src/Util/Factorize.vo (real: 0.44, user: 0.32, sys: 0.12, mem: 369692 ko)
COQC src/Util/ZUtil/Pow2.v
src/Util/ZUtil/Pow2.vo (real: 0.43, user: 0.30, sys: 0.13, mem: 367256 ko)
COQC src/Util/ZUtil/ZSimplify/Simple.v
src/Util/ZUtil/ZSimplify/Simple.vo (real: 0.47, user: 0.30, sys: 0.17, mem: 411064 ko)
COQC src/Util/ZUtil/Tactics/PeelLe.v
src/Util/ZUtil/Tactics/PeelLe.vo (real: 0.40, user: 0.31, sys: 0.08, mem: 342236 ko)
COQC src/Util/NatUtil.v
src/Util/NatUtil.vo (real: 2.07, user: 1.87, sys: 0.19, mem: 458424 ko)
COQC src/Util/Tactics/PrintContext.v
src/Util/Tactics/PrintContext.vo (real: 0.06, user: 0.03, sys: 0.03, mem: 63364 ko)
COQC src/Util/Tactics/NormalizeCommutativeIdentifier.v
src/Util/Tactics/NormalizeCommutativeIdentifier.vo (real: 0.06, user: 0.03, sys: 0.03, mem: 63272 ko)
COQC src/Util/ZUtil/Tactics/SplitMinMax.v
src/Util/ZUtil/Tactics/SplitMinMax.vo (real: 0.39, user: 0.30, sys: 0.09, mem: 340484 ko)
COQC src/Util/Tactics/SetEvars.v
src/Util/Tactics/SetEvars.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 63108 ko)
COQC src/Util/Tactics/SubstEvars.v
src/Util/Tactics/SubstEvars.vo (real: 0.06, user: 0.01, sys: 0.04, mem: 63164 ko)
COQC src/Util/PER.v
src/Util/PER.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 74472 ko)
COQC src/Util/ZUtil/N2Z.v
src/Util/ZUtil/N2Z.vo (real: 0.43, user: 0.32, sys: 0.11, mem: 378708 ko)
COQC src/Util/FueledLUB.v
src/Util/FueledLUB.vo (real: 0.06, user: 0.03, sys: 0.02, mem: 63652 ko)
COQC src/Util/Tactics/SimplifyRepeatedIfs.v
src/Util/Tactics/SimplifyRepeatedIfs.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 63388 ko)
COQC src/Util/Tactics/ETransitivity.v
src/Util/Tactics/ETransitivity.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 68848 ko)
COQC src/Util/Tactics/SubstLet.v
src/Util/Tactics/SubstLet.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 63036 ko)
COQC src/Util/ZUtil/Lnot.v
src/Util/ZUtil/Lnot.vo (real: 0.40, user: 0.30, sys: 0.09, mem: 347364 ko)
COQC src/TAPSort.v
src/TAPSort.vo (real: 0.42, user: 0.28, sys: 0.14, mem: 362040 ko)
COQC src/Util/ZUtil/Z2Nat.v
src/Util/ZUtil/Z2Nat.vo (real: 0.44, user: 0.32, sys: 0.12, mem: 399724 ko)
COQC src/Util/ZUtil/ModExp.v
src/Util/ZUtil/ModExp.vo (real: 0.41, user: 0.31, sys: 0.10, mem: 348960 ko)
COQC src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised.v
src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo (real: 1.73, user: 1.58, sys: 0.15, mem: 463148 ko)
COQC src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.v
src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo (real: 1.72, user: 1.60, sys: 0.11, mem: 462756 ko)
COQC src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.v
src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo (real: 1.61, user: 1.47, sys: 0.13, mem: 460804 ko)
COQC src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.v
src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo (real: 4.18, user: 4.01, sys: 0.16, mem: 569084 ko)
COQC src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v
src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo (real: 7.05, user: 6.80, sys: 0.25, mem: 681856 ko)
COQC src/Util/Loops.v
src/Util/Loops.vo (real: 0.82, user: 0.68, sys: 0.13, mem: 439640 ko)
COQC src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.v
src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo (real: 6.77, user: 6.57, sys: 0.19, mem: 676780 ko)
COQC src/PushButtonSynthesis/InvertHighLow.v
src/PushButtonSynthesis/InvertHighLow.vo (real: 0.35, user: 0.25, sys: 0.09, mem: 295228 ko)
COQC src/Util/ChangeInAll.v
src/Util/ChangeInAll.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 63164 ko)
COQC src/Util/Tactics/ChangeInAll.v
src/Util/Tactics/ChangeInAll.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 63296 ko)
COQC src/Util/DefaultedTypes.v
src/Util/DefaultedTypes.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 63356 ko)
COQC src/Util/Pos.v
src/Util/Pos.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 64952 ko)
COQC src/Util/Sumbool.v
src/Util/Sumbool.vo (real: 0.09, user: 0.05, sys: 0.03, mem: 87752 ko)
COQC src/Util/Tactics/TransparentAssert.v
src/Util/Tactics/TransparentAssert.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 63832 ko)
COQC src/Util/Tactics/EvarNormalize.v
src/Util/Tactics/EvarNormalize.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 63300 ko)
COQC src/Util/Tactics/ClearAll.v
src/Util/Tactics/ClearAll.vo (real: 0.07, user: 0.05, sys: 0.01, mem: 63224 ko)
COQC src/Util/Tactics/ClearDuplicates.v
src/Util/Tactics/ClearDuplicates.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 63380 ko)
COQC src/Util/Tactics/ClearbodyAll.v
src/Util/Tactics/ClearbodyAll.vo (real: 0.06, user: 0.03, sys: 0.03, mem: 62964 ko)
COQC src/Util/Tactics/ConvoyDestruct.v
src/Util/Tactics/ConvoyDestruct.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 64008 ko)
COQC src/Util/Tactics/CPSId.v
src/Util/Tactics/CPSId.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 65512 ko)
COQC src/Util/Tactics/DestructTrivial.v
src/Util/Tactics/DestructTrivial.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 63368 ko)
COQC src/Util/Tactics/ESpecialize.v
src/Util/Tactics/ESpecialize.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 63096 ko)
COQC src/Util/Tactics/EvarExists.v
src/Util/Tactics/EvarExists.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 62888 ko)
COQC src/Util/Tactics/Forward.v
src/Util/Tactics/Forward.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 63720 ko)
COQC src/Util/Tactics/PoseTermWithName.v
src/Util/Tactics/PoseTermWithName.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 63108 ko)
COQC src/Util/Tactics/SideConditionsBeforeToAfter.v
src/Util/Tactics/SideConditionsBeforeToAfter.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 63244 ko)
COQC src/Util/Tactics/SimplifyProjections.v
src/Util/Tactics/SimplifyProjections.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 64360 ko)
COQC src/Util/Tactics/UnfoldArg.v
src/Util/Tactics/UnfoldArg.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 63488 ko)
COQC src/Util/Tactics/UnifyAbstractReflexivity.v
src/Util/Tactics/UnifyAbstractReflexivity.vo (real: 0.07, user: 0.05, sys: 0.01, mem: 64560 ko)
COQC src/Util/Tactics/VM.v
src/Util/Tactics/VM.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 64140 ko)
COQC src/Util/Unit.v
src/Util/Unit.vo (real: 0.07, user: 0.05, sys: 0.02, mem: 71720 ko)
COQC src/Util/Bool/IsTrue.v
src/Util/Bool/IsTrue.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 65244 ko)
COQC src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.v
src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo (real: 7.74, user: 7.53, sys: 0.21, mem: 710380 ko)
COQC src/Util/ZUtil/Ge.v
src/Util/ZUtil/Ge.vo (real: 0.35, user: 0.22, sys: 0.12, mem: 311944 ko)
COQC src/Util/ZUtil/DistrIf.v
src/Util/ZUtil/DistrIf.vo (real: 0.43, user: 0.32, sys: 0.10, mem: 357700 ko)
COQC src/Util/ZUtil/Mul.v
src/Util/ZUtil/Mul.vo (real: 0.41, user: 0.29, sys: 0.11, mem: 342396 ko)
COQC src/Util/SideConditions/CorePackages.v
src/Util/SideConditions/CorePackages.vo (real: 0.08, user: 0.05, sys: 0.02, mem: 72428 ko)
COQC src/Util/Logic/ImplAnd.v
src/Util/Logic/ImplAnd.vo (real: 0.07, user: 0.05, sys: 0.01, mem: 70644 ko)
COQC src/Util/Sigma/Associativity.v
src/Util/Sigma/Associativity.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 65640 ko)
COQC src/Util/Sigma/Lift.v
src/Util/Sigma/Lift.vo (real: 0.08, user: 0.05, sys: 0.02, mem: 83076 ko)
COQC src/Util/ZUtil/Sgn.v
src/Util/ZUtil/Sgn.vo (real: 0.44, user: 0.33, sys: 0.10, mem: 378096 ko)
COQC src/Util/Sigma/MapProjections.v
src/Util/Sigma/MapProjections.vo (real: 0.08, user: 0.05, sys: 0.02, mem: 65192 ko)
cp -f AUTHORS fiat-rust/AUTHORS
cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS
cp -f COPYRIGHT fiat-rust/COPYRIGHT
cp -f LICENSE-MIT fiat-rust/LICENSE-MIT
COQC src/Util/ZUtil/Sorting.v
src/Util/ZUtil/Sorting.vo (real: 0.43, user: 0.32, sys: 0.10, mem: 355432 ko)
cp -f LICENSE-APACHE fiat-rust/LICENSE-APACHE
cp -f LICENSE-BSD-1 fiat-rust/LICENSE-BSD-1
cp -f AUTHORS fiat-go/AUTHORS
cp -f CONTRIBUTORS fiat-go/CONTRIBUTORS
cp -f COPYRIGHT fiat-go/COPYRIGHT
cp -f LICENSE-MIT fiat-go/LICENSE-MIT
cp -f LICENSE-APACHE fiat-go/LICENSE-APACHE
cp -f LICENSE-BSD-1 fiat-go/LICENSE-BSD-1
COQC src/Util/Sigma/Related.v
src/Util/Sigma/Related.vo (real: 0.12, user: 0.08, sys: 0.04, mem: 118132 ko)
COQC src/Util/FixCoqMistakes.v
src/Util/FixCoqMistakes.vo (real: 0.08, user: 0.05, sys: 0.03, mem: 76908 ko)
COQC src/Util/Tactics/Not.v
src/Util/Tactics/Not.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 63496 ko)
COQC src/Util/Equality.v
src/Util/Equality.vo (real: 0.15, user: 0.09, sys: 0.05, mem: 145440 ko)
COQC src/Util/Tactics/SetoidSubst.v
src/Util/Tactics/SetoidSubst.vo (real: 0.07, user: 0.05, sys: 0.02, mem: 64488 ko)
COQC src/Util/Tactics/RunTacticAsConstr.v
src/Util/Tactics/RunTacticAsConstr.vo (real: 0.07, user: 0.03, sys: 0.04, mem: 70372 ko)
COQC src/Util/Logic/Forall.v
src/Util/Logic/Forall.vo (real: 0.08, user: 0.04, sys: 0.03, mem: 76272 ko)
COQC src/Util/Structures/Equalities/Iso.v
src/Util/Structures/Equalities/Iso.vo (real: 0.13, user: 0.09, sys: 0.04, mem: 118404 ko)
COQC src/Util/Logic/Exists.v
src/Util/Logic/Exists.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 73892 ko)
COQC src/Util/ZUtil/Div/Bootstrap.v
src/Util/ZUtil/Div/Bootstrap.vo (real: 0.43, user: 0.30, sys: 0.12, mem: 343324 ko)
COQC src/Util/ZUtil/Modulo/Bootstrap.v
src/Util/ZUtil/Modulo/Bootstrap.vo (real: 0.43, user: 0.28, sys: 0.14, mem: 356256 ko)
COQC src/Algebra/Nsatz.v
src/Algebra/Nsatz.vo (real: 0.52, user: 0.39, sys: 0.13, mem: 418824 ko)
COQC src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v
src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo (real: 10.76, user: 10.51, sys: 0.25, mem: 849756 ko)
COQC src/Util/ZUtil/Hints/ZArith.v
src/Util/ZUtil/Hints/ZArith.vo (real: 0.41, user: 0.32, sys: 0.08, mem: 343492 ko)
COQC src/Util/ZUtil/Hints/PullPush.v
src/Util/ZUtil/Hints/PullPush.vo (real: 0.43, user: 0.29, sys: 0.13, mem: 351924 ko)
COQC src/Util/ZUtil/Hints/Ztestbit.v
src/Util/ZUtil/Hints/Ztestbit.vo (real: 0.41, user: 0.33, sys: 0.08, mem: 342284 ko)
COQC src/Util/ZUtil/ZSimplify/Core.v
src/Util/ZUtil/ZSimplify/Core.vo (real: 0.41, user: 0.27, sys: 0.14, mem: 348184 ko)
COQC src/Util/Logic.v
src/Util/Logic.vo (real: 0.09, user: 0.05, sys: 0.03, mem: 86660 ko)
COQC src/Util/Tactics/UniquePose.v
src/Util/Tactics/UniquePose.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 71188 ko)
COQC src/Util/Tactics/CountBinders.v
src/Util/Tactics/CountBinders.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 70920 ko)
COQC src/Util/Tactics/AppendUnderscores.v
src/Util/Tactics/AppendUnderscores.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 70124 ko)
COQC src/Util/DynList.v
src/Util/DynList.vo (real: 0.15, user: 0.08, sys: 0.06, mem: 149268 ko)
COQC src/Util/Tactics/PrintGoal.v
src/Util/Tactics/PrintGoal.vo (real: 0.06, user: 0.04, sys: 0.02, mem: 63408 ko)
COQC src/Util/Logic/ProdForall.v
src/Util/Logic/ProdForall.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 83900 ko)
COQC src/Util/Telescope/Core.v
src/Util/Telescope/Core.vo (real: 0.10, user: 0.07, sys: 0.02, mem: 102120 ko)
COQC src/Util/Curry.v
src/Util/Curry.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 66928 ko)
COQC src/Util/ZUtil/Tactics/LinearSubstitute.v
src/Util/ZUtil/Tactics/LinearSubstitute.vo (real: 0.45, user: 0.31, sys: 0.13, mem: 374168 ko)
COQC src/Util/Tactics/CacheTerm.v
src/Util/Tactics/CacheTerm.vo (real: 0.07, user: 0.03, sys: 0.04, mem: 65992 ko)
COQC src/Util/Tower.v
src/Util/Tower.vo (real: 0.08, user: 0.05, sys: 0.03, mem: 83912 ko)
COQC src/Util/ZUtil/Opp.v
src/Util/ZUtil/Opp.vo (real: 0.44, user: 0.31, sys: 0.13, mem: 349424 ko)
COQC src/Util/Tactics/HeadUnderBinders.v
src/Util/Tactics/HeadUnderBinders.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 70608 ko)
COQC src/Util/ZUtil/Nat2Z.v
src/Util/ZUtil/Nat2Z.vo (real: 0.45, user: 0.32, sys: 0.12, mem: 382708 ko)
COQC src/Util/Notations.v
src/Util/Notations.vo (real: 0.08, user: 0.05, sys: 0.03, mem: 83244 ko)
COQC src/Util/Tactics/Head.v
src/Util/Tactics/Head.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 70528 ko)
COQC src/Util/Tactics/DestructHyps.v
src/Util/Tactics/DestructHyps.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 72256 ko)
COQC src/Util/Prod.v
src/Util/Prod.vo (real: 0.23, user: 0.15, sys: 0.07, mem: 263912 ko)
COQC src/Util/Strings/String_as_OT_old.v
src/Util/Strings/String_as_OT_old.vo (real: 0.59, user: 0.47, sys: 0.11, mem: 420476 ko)
COQC src/Util/Tactics/SpecializeBy.v
src/Util/Tactics/SpecializeBy.vo (real: 0.07, user: 0.05, sys: 0.01, mem: 71320 ko)
COQC src/Util/Wf.v
src/Util/Wf.vo (real: 0.69, user: 0.54, sys: 0.14, mem: 369764 ko)
COQC src/Util/Tactics/DoWithHyp.v
src/Util/Tactics/DoWithHyp.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 70680 ko)
COQC src/Util/Tactics/SplitInContext.v
src/Util/Tactics/SplitInContext.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 71628 ko)
COQC src/Util/Sigma.v
src/Util/Sigma.vo (real: 0.23, user: 0.17, sys: 0.06, mem: 240532 ko)
COQC src/Util/Bool.v
src/Util/Bool.vo (real: 0.15, user: 0.10, sys: 0.05, mem: 157660 ko)
COQC src/Util/PrimitiveProd.v
src/Util/PrimitiveProd.vo (real: 0.18, user: 0.10, sys: 0.08, mem: 197864 ko)
COQC src/Util/LetIn.v
src/Util/LetIn.vo (real: 0.09, user: 0.06, sys: 0.03, mem: 92956 ko)
COQC src/Util/ErrorT.v
src/Util/ErrorT.vo (real: 0.08, user: 0.04, sys: 0.03, mem: 76776 ko)
COQC src/Util/CPSNotations.v
src/Util/CPSNotations.vo (real: 0.08, user: 0.06, sys: 0.02, mem: 77372 ko)
COQC src/Util/ZUtil/Notations.v
src/Util/ZUtil/Notations.vo (real: 0.23, user: 0.18, sys: 0.05, mem: 229792 ko)
COQC src/Util/PrimitiveHList.v
src/Util/PrimitiveHList.vo (real: 0.15, user: 0.11, sys: 0.04, mem: 156976 ko)
COQC src/Util/Strings/String_as_OT.v
src/Util/Strings/String_as_OT.vo (real: 1.15, user: 0.99, sys: 0.15, mem: 451068 ko)
COQC src/Util/Structures/Orders/Iso.v
src/Util/Structures/Orders/Iso.vo (real: 0.11, user: 0.07, sys: 0.03, mem: 105976 ko)
COQC src/Util/Compose.v
src/Util/Compose.vo (real: 0.10, user: 0.06, sys: 0.04, mem: 101192 ko)
COQC src/Util/ListUtil/FoldBool.v
src/Util/ListUtil/FoldBool.vo (real: 0.35, user: 0.25, sys: 0.10, mem: 352652 ko)
COQC src/Util/ZUtil/Tactics/LtbToLt.v
src/Util/ZUtil/Tactics/LtbToLt.vo (real: 0.52, user: 0.38, sys: 0.13, mem: 438344 ko)
COQC src/Util/ZUtil/Tactics/DivModToQuotRem.v
src/Util/ZUtil/Tactics/DivModToQuotRem.vo (real: 0.42, user: 0.28, sys: 0.13, mem: 343476 ko)
COQC src/Util/ZUtil/Hints.v
src/Util/ZUtil/Hints.vo (real: 0.41, user: 0.32, sys: 0.09, mem: 345896 ko)
COQC src/Util/Tactics/SpecializeAllWays.v
src/Util/Tactics/SpecializeAllWays.vo (real: 0.07, user: 0.04, sys: 0.02, mem: 70764 ko)
COQC src/Util/Relations.v
src/Util/Relations.vo (real: 0.17, user: 0.09, sys: 0.07, mem: 189188 ko)
COQC src/Util/Tactics/AllSuccesses.v
src/Util/Tactics/AllSuccesses.vo (real: 0.14, user: 0.10, sys: 0.03, mem: 146172 ko)
COQC src/Util/Telescope/Instances.v
src/Util/Telescope/Instances.vo (real: 0.18, user: 0.14, sys: 0.03, mem: 193176 ko)
COQC src/Util/PointedProp.v
src/Util/PointedProp.vo (real: 0.31, user: 0.24, sys: 0.07, mem: 311876 ko)
COQC src/Util/AutoRewrite.v
src/Util/AutoRewrite.vo (real: 0.08, user: 0.05, sys: 0.03, mem: 82996 ko)
COQC src/Util/ZUtil/Modulo/PullPush.v
src/Util/ZUtil/Modulo/PullPush.vo (real: 0.81, user: 0.68, sys: 0.12, mem: 440168 ko)
COQC src/Util/LetInMonad.v
src/Util/LetInMonad.vo (real: 0.28, user: 0.20, sys: 0.08, mem: 302984 ko)
COQC src/Util/ParseTaps.v
src/Util/ParseTaps.vo (real: 0.25, user: 0.20, sys: 0.05, mem: 240680 ko)
COQC src/Util/Tactics/MoveLetIn.v
src/Util/Tactics/MoveLetIn.vo (real: 0.08, user: 0.04, sys: 0.03, mem: 75048 ko)
COQC src/Util/PrimitiveSigma.v
src/Util/PrimitiveSigma.vo (real: 0.17, user: 0.12, sys: 0.04, mem: 165508 ko)
COQC src/Util/TagList.v
src/Util/TagList.vo (real: 0.16, user: 0.09, sys: 0.06, mem: 157184 ko)
COQC src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.v
src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo (real: 8.89, user: 8.65, sys: 0.23, mem: 787528 ko)
COQC src/Util/SideConditions/RingPackage.v
src/Util/SideConditions/RingPackage.vo (real: 0.34, user: 0.25, sys: 0.09, mem: 298356 ko)
COQC src/Util/Strings/Ascii.v
src/Util/Strings/Ascii.vo (real: 0.31, user: 0.23, sys: 0.07, mem: 279804 ko)
COQC src/Util/Strings/StringMap.v
src/Util/Strings/StringMap.vo (real: 0.49, user: 0.35, sys: 0.13, mem: 425712 ko)
COQC src/Util/Tactics/BreakMatch.v
src/Util/Tactics/BreakMatch.vo (real: 0.08, user: 0.05, sys: 0.02, mem: 74852 ko)
COQC src/Util/Strings/Sorting.v
src/Util/Strings/Sorting.vo (real: 0.65, user: 0.53, sys: 0.12, mem: 443612 ko)
COQC src/Util/Tactics/DestructHead.v
src/Util/Tactics/DestructHead.vo (real: 0.09, user: 0.05, sys: 0.03, mem: 79100 ko)
COQC src/Util/Tactics/RewriteHyp.v
src/Util/Tactics/RewriteHyp.vo (real: 0.10, user: 0.04, sys: 0.05, mem: 90228 ko)
COQC src/Util/ZUtil/Tactics/PullPush/Modulo.v
src/Util/ZUtil/Tactics/PullPush/Modulo.vo (real: 0.45, user: 0.31, sys: 0.13, mem: 348300 ko)
COQC src/Util/ZUtil/Le.v
src/Util/ZUtil/Le.vo (real: 0.55, user: 0.38, sys: 0.17, mem: 439536 ko)
COQC src/Util/Decidable.v
src/Util/Decidable.vo (real: 0.68, user: 0.58, sys: 0.10, mem: 397472 ko)
COQC src/Util/Tactics/AllInstances.v
src/Util/Tactics/AllInstances.vo (real: 0.15, user: 0.09, sys: 0.05, mem: 147180 ko)
COQC src/Util/ListUtil/ForallIn.v
src/Util/ListUtil/ForallIn.vo (real: 0.20, user: 0.13, sys: 0.07, mem: 219788 ko)
COQC src/Util/ZUtil/Tactics/RewriteModSmall.v
src/Util/ZUtil/Tactics/RewriteModSmall.vo (real: 0.47, user: 0.36, sys: 0.10, mem: 402532 ko)
COQC src/Util/ZUtil/Tactics/PullPush.v
src/Util/ZUtil/Tactics/PullPush.vo (real: 0.36, user: 0.25, sys: 0.10, mem: 312824 ko)
COQC src/Util/Telescope/Equality.v
src/Util/Telescope/Equality.vo (real: 0.23, user: 0.14, sys: 0.08, mem: 273156 ko)
COQC src/Util/Tactics.v
src/Util/Tactics.vo (real: 0.16, user: 0.09, sys: 0.06, mem: 166272 ko)
COQC src/Util/SideConditions/ReductionPackages.v
src/Util/SideConditions/ReductionPackages.vo (real: 0.26, user: 0.17, sys: 0.08, mem: 248560 ko)
COQC src/Util/Logic/ExistsEqAnd.v
src/Util/Logic/ExistsEqAnd.vo (real: 0.10, user: 0.06, sys: 0.04, mem: 102004 ko)
COQC src/Util/FMapPositive/Equality.v
src/Util/FMapPositive/Equality.vo (real: 0.39, user: 0.30, sys: 0.09, mem: 372252 ko)
COQC src/Util/PartiallyReifiedProp.v
src/Util/PartiallyReifiedProp.vo (real: 0.87, user: 0.77, sys: 0.10, mem: 322204 ko)
COQC src/Util/MSetPositive/Equality.v
src/Util/MSetPositive/Equality.vo (real: 0.54, user: 0.40, sys: 0.13, mem: 426740 ko)
COQC src/Util/Strings/String.v
src/Util/Strings/String.vo (real: 0.57, user: 0.43, sys: 0.13, mem: 436720 ko)
COQC src/Util/Option.v
src/Util/Option.vo (real: 0.37, user: 0.29, sys: 0.08, mem: 312716 ko)
COQC src/Util/ZUtil/Definitions.v
src/Util/ZUtil/Definitions.vo (real: 0.37, user: 0.26, sys: 0.10, mem: 331272 ko)
COQC src/Algebra/Hierarchy.v
src/Algebra/Hierarchy.vo (real: 0.34, user: 0.24, sys: 0.09, mem: 309752 ko)
COQC src/Util/Sum.v
src/Util/Sum.vo (real: 0.60, user: 0.47, sys: 0.13, mem: 399408 ko)
COQC src/Util/ZUtil/Peano.v
src/Util/ZUtil/Peano.vo (real: 0.50, user: 0.40, sys: 0.10, mem: 437660 ko)
COQC src/Util/NUtil/WithoutReferenceToZ.v
src/Util/NUtil/WithoutReferenceToZ.vo (real: 0.51, user: 0.39, sys: 0.12, mem: 441376 ko)
COQC src/Util/ZUtil/Ltz.v
src/Util/ZUtil/Ltz.vo (real: 0.79, user: 0.66, sys: 0.13, mem: 447236 ko)
COQC src/Util/ZUtil/MulSplit.v
src/Util/ZUtil/MulSplit.vo (real: 0.46, user: 0.34, sys: 0.12, mem: 394312 ko)
COQC src/Util/ZUtil/AddModulo.v
src/Util/ZUtil/AddModulo.vo (real: 0.35, user: 0.23, sys: 0.12, mem: 309872 ko)
COQC src/Util/ZUtil/ZSimplify/Autogenerated.v
src/Util/ZUtil/ZSimplify/Autogenerated.vo (real: 5.87, user: 5.75, sys: 0.11, mem: 470956 ko)
COQC src/Util/ZUtil/Combine.v
src/Util/ZUtil/Combine.vo (real: 0.57, user: 0.42, sys: 0.15, mem: 444348 ko)
COQC src/Spec/MxDH.v
src/Spec/MxDH.vo (real: 0.29, user: 0.19, sys: 0.09, mem: 276016 ko)
COQC src/Util/ListUtil/Forall.v
src/Util/ListUtil/Forall.vo (real: 1.34, user: 1.20, sys: 0.14, mem: 443904 ko)
COQC src/Util/ZUtil/CPS.v
src/Util/ZUtil/CPS.vo (real: 0.62, user: 0.49, sys: 0.12, mem: 442660 ko)
COQC src/Util/ZUtil/LnotModulo.v
src/Util/ZUtil/LnotModulo.vo (real: 0.34, user: 0.20, sys: 0.14, mem: 309600 ko)
COQC src/Util/Wf1.v
src/Util/Wf1.vo (real: 1.28, user: 1.15, sys: 0.13, mem: 372288 ko)
COQC src/Util/Structures/Equalities/Sum.v
src/Util/Structures/Equalities/Sum.vo (real: 0.33, user: 0.23, sys: 0.09, mem: 326420 ko)
COQC src/Util/ZUtil/Zselect.v
src/Util/ZUtil/Zselect.vo (real: 0.34, user: 0.25, sys: 0.08, mem: 319540 ko)
COQC src/Util/ListUtil/SetoidList.v
src/Util/ListUtil/SetoidList.vo (real: 0.39, user: 0.25, sys: 0.14, mem: 354448 ko)
COQC src/Util/OptionList.v
src/Util/OptionList.vo (real: 0.85, user: 0.71, sys: 0.14, mem: 441596 ko)
COQC src/Algebra/Monoid.v
src/Algebra/Monoid.vo (real: 0.47, user: 0.29, sys: 0.17, mem: 399684 ko)
COQC src/Util/ZUtil/ZSimplify.v
src/Util/ZUtil/ZSimplify.vo (real: 0.37, user: 0.28, sys: 0.09, mem: 318228 ko)
COQC src/Util/ZUtil/AddGetCarry.v
src/Util/ZUtil/AddGetCarry.vo (real: 1.28, user: 1.13, sys: 0.14, mem: 452096 ko)
COQC src/Util/MSetPositive/Facts.v
src/Util/MSetPositive/Facts.vo (real: 0.63, user: 0.51, sys: 0.12, mem: 449888 ko)
COQC src/Util/Strings/Parse/Common.v
src/Util/Strings/Parse/Common.vo (real: 0.43, user: 0.33, sys: 0.10, mem: 367916 ko)
COQC src/Util/Wf2.v
src/Util/Wf2.vo (real: 2.39, user: 2.25, sys: 0.13, mem: 389416 ko)
COQC src/Util/ZUtil/ModInv.v
src/Util/ZUtil/ModInv.vo (real: 2.57, user: 2.39, sys: 0.17, mem: 477872 ko)
COQC src/Util/Structures/Orders/Sum.v
src/Util/Structures/Orders/Sum.vo (real: 0.80, user: 0.67, sys: 0.13, mem: 400300 ko)
COQC src/Util/SideConditions/ModInvPackage.v
src/Util/SideConditions/ModInvPackage.vo (real: 0.46, user: 0.37, sys: 0.09, mem: 384060 ko)
COQC src/Util/ZUtil/Rshi.v
src/Util/ZUtil/Rshi.vo (real: 1.35, user: 1.17, sys: 0.17, mem: 449144 ko)
COQC src/Util/Strings/ParseArithmetic.v
src/Util/Strings/ParseArithmetic.vo (real: 0.79, user: 0.63, sys: 0.15, mem: 453656 ko)
COQC src/Util/SideConditions/Autosolve.v
src/Util/SideConditions/Autosolve.vo (real: 0.43, user: 0.29, sys: 0.13, mem: 359864 ko)
COQC src/Util/Strings/ParseArithmeticToTaps.v
src/Util/Strings/ParseArithmeticToTaps.vo (real: 0.75, user: 0.59, sys: 0.16, mem: 450284 ko)
COQC src/Algebra/Group.v
src/Algebra/Group.vo (real: 3.72, user: 3.58, sys: 0.14, mem: 416660 ko)
COQC src/Util/ListUtil.v
src/Util/ListUtil.vo (real: 8.25, user: 8.11, sys: 0.14, mem: 510360 ko)
COQC src/Algebra/ScalarMult.v
src/Algebra/ScalarMult.vo (real: 1.64, user: 1.50, sys: 0.13, mem: 450856 ko)
COQC src/Util/Bool/Reflect.v
src/Util/Bool/Reflect.vo (real: 1.83, user: 1.67, sys: 0.16, mem: 466136 ko)
COQC src/Util/Tuple.v
src/Util/Tuple.vo (real: 1.97, user: 1.84, sys: 0.13, mem: 469740 ko)
COQC src/Util/ZUtil/Pow.v
src/Util/ZUtil/Pow.vo (real: 0.60, user: 0.45, sys: 0.14, mem: 454696 ko)
COQC src/Arithmetic/BarrettReduction/RidiculousFish.v
src/Arithmetic/BarrettReduction/RidiculousFish.vo (real: 17.85, user: 17.73, sys: 0.11, mem: 467984 ko)
COQC src/MiscCompilerPasses.v
src/MiscCompilerPasses.vo (real: 1.10, user: 0.90, sys: 0.19, mem: 506608 ko)
COQC src/Util/IdfunWithAlt.v
src/Util/IdfunWithAlt.vo (real: 0.48, user: 0.37, sys: 0.11, mem: 412112 ko)
COQC src/Util/MSets/Iso.v
src/Util/MSets/Iso.vo (real: 3.16, user: 3.00, sys: 0.16, mem: 488720 ko)
COQC src/Util/AdditionChainExponentiation.v
src/Util/AdditionChainExponentiation.vo (real: 0.58, user: 0.43, sys: 0.14, mem: 457096 ko)
COQC src/Util/HList.v
src/Util/HList.vo (real: 0.68, user: 0.52, sys: 0.16, mem: 456444 ko)
COQC src/Fancy/Spec.v
src/Fancy/Spec.vo (real: 1.45, user: 1.32, sys: 0.12, mem: 489920 ko)
COQC src/Util/Decidable/Decidable2Bool.v
src/Util/Decidable/Decidable2Bool.vo (real: 0.78, user: 0.66, sys: 0.12, mem: 457296 ko)
COQC src/Util/Level.v
src/Util/Level.vo (real: 0.66, user: 0.54, sys: 0.12, mem: 454468 ko)
COQC src/Util/Listable.v
src/Util/Listable.vo (real: 0.63, user: 0.50, sys: 0.12, mem: 454808 ko)
COQC src/Util/ZRange.v
src/Util/ZRange.vo (real: 0.64, user: 0.51, sys: 0.13, mem: 457192 ko)
COQC src/Util/ZUtil/Log2.v
src/Util/ZUtil/Log2.vo (real: 0.71, user: 0.58, sys: 0.13, mem: 457856 ko)
COQC src/Util/ZUtil/Div.v
src/Util/ZUtil/Div.vo (real: 2.55, user: 2.41, sys: 0.14, mem: 475580 ko)
COQC src/Util/MSets/Sum.v
src/Util/MSets/Sum.vo (real: 6.91, user: 6.75, sys: 0.15, mem: 503036 ko)
COQC src/Util/ZBounded.v
src/Util/ZBounded.vo (real: 0.68, user: 0.54, sys: 0.13, mem: 457860 ko)
COQC src/Util/CPSUtil.v
src/Util/CPSUtil.vo (real: 0.93, user: 0.81, sys: 0.12, mem: 459596 ko)
COQC src/Util/Strings/Show.v
src/Util/Strings/Show.vo (real: 0.71, user: 0.54, sys: 0.17, mem: 463188 ko)
COQC src/Util/ZRange/Operations.v
src/Util/ZRange/Operations.vo (real: 0.62, user: 0.47, sys: 0.15, mem: 458004 ko)
COQC src/Assembly/Syntax.v
src/Assembly/Syntax.vo (real: 5.42, user: 5.16, sys: 0.26, mem: 714352 ko)
COQC src/MiscCompilerPassesProofs.v
src/MiscCompilerPassesProofs.vo (real: 3.24, user: 3.08, sys: 0.15, mem: 523284 ko)
COQC src/Util/ZUtil/Tactics/ZeroBounds.v
src/Util/ZUtil/Tactics/ZeroBounds.vo (real: 0.50, user: 0.37, sys: 0.12, mem: 415832 ko)
COQC src/Util/ZUtil/Divide.v
src/Util/ZUtil/Divide.vo (real: 0.63, user: 0.46, sys: 0.16, mem: 461316 ko)
COQC src/Algebra/Ring.v
src/Algebra/Ring.vo (real: 11.46, user: 11.30, sys: 0.15, mem: 502592 ko)
COQC src/Util/ErrorT/Show.v
src/Util/ErrorT/Show.vo (real: 0.56, user: 0.43, sys: 0.12, mem: 465024 ko)
COQC src/Util/ZUtil/Tactics/SimplifyFractionsLe.v
src/Util/ZUtil/Tactics/SimplifyFractionsLe.vo (real: 0.50, user: 0.37, sys: 0.12, mem: 419300 ko)
COQC src/Util/Arg.v
src/Util/Arg.vo (real: 0.93, user: 0.80, sys: 0.12, mem: 473944 ko)
COQC src/Assembly/Equality.v
src/Assembly/Equality.vo (real: 0.89, user: 0.72, sys: 0.16, mem: 485092 ko)
COQC src/Language/PreExtra.v
src/Language/PreExtra.vo (real: 0.64, user: 0.46, sys: 0.18, mem: 467664 ko)
COQC src/Util/Strings/NamingConventions.v
src/Util/Strings/NamingConventions.vo (real: 0.74, user: 0.63, sys: 0.10, mem: 467548 ko)
COQC src/Util/ZRange/Show.v
src/Util/ZRange/Show.vo (real: 0.60, user: 0.41, sys: 0.18, mem: 466416 ko)
COQC src/Util/MSets/Show.v
src/Util/MSets/Show.vo (real: 0.61, user: 0.45, sys: 0.15, mem: 467860 ko)
COQC src/Algebra/IntegralDomain.v
src/Algebra/IntegralDomain.vo (real: 1.00, user: 0.83, sys: 0.17, mem: 460260 ko)
COQC src/Assembly/Semantics.v
src/Assembly/Semantics.vo (real: 3.51, user: 3.33, sys: 0.17, mem: 544744 ko)
COQC src/Util/ZUtil/Testbit.v
src/Util/ZUtil/Testbit.vo (real: 2.20, user: 2.05, sys: 0.15, mem: 467888 ko)
COQC src/Util/ZUtil/Ones.v
src/Util/ZUtil/Ones.vo (real: 1.39, user: 1.21, sys: 0.18, mem: 463596 ko)
COQC src/Util/ZUtil/CC.v
src/Util/ZUtil/CC.vo (real: 0.91, user: 0.77, sys: 0.14, mem: 466460 ko)
COQC src/Algebra/SubsetoidRing.v
src/Algebra/SubsetoidRing.vo (real: 0.88, user: 0.71, sys: 0.17, mem: 461184 ko)
COQC src/Rewriter/Rules.v
src/Rewriter/Rules.vo (real: 1.14, user: 1.00, sys: 0.13, mem: 482280 ko)
COQC src/Rewriter/TestRules.v
src/Rewriter/TestRules.vo (real: 0.66, user: 0.51, sys: 0.14, mem: 471512 ko)
COQC src/Util/ZUtil/Tactics/Ztestbit.v
src/Util/ZUtil/Tactics/Ztestbit.vo (real: 0.51, user: 0.39, sys: 0.12, mem: 424264 ko)
COQC src/Util/ZRange/BasicLemmas.v
src/Util/ZRange/BasicLemmas.vo (real: 6.11, user: 5.97, sys: 0.14, mem: 502384 ko)
COQC src/Language/IdentifierParameters.v
src/Language/IdentifierParameters.vo (real: 0.65, user: 0.48, sys: 0.16, mem: 471192 ko)
COQC src/Util/MSetPositive/Show.v
src/Util/MSetPositive/Show.vo (real: 0.77, user: 0.64, sys: 0.12, mem: 489572 ko)
COQC src/Util/ZUtil/Land.v
src/Util/ZUtil/Land.vo (real: 0.68, user: 0.53, sys: 0.14, mem: 461624 ko)
COQC src/Assembly/Parse.v
src/Assembly/Parse.vo (real: 2.10, user: 1.91, sys: 0.19, mem: 509460 ko)
COQC src/Util/ZUtil/Tactics/SolveTestbit.v
src/Util/ZUtil/Tactics/SolveTestbit.vo (real: 0.60, user: 0.43, sys: 0.16, mem: 461948 ko)
COQC src/Util/ZUtil/Lor.v
src/Util/ZUtil/Lor.vo (real: 0.60, user: 0.42, sys: 0.17, mem: 461608 ko)
COQC src/Util/ZUtil/Stabilization.v
src/Util/ZUtil/Stabilization.vo (real: 0.85, user: 0.68, sys: 0.17, mem: 467216 ko)
COQC src/Util/ZUtil/Modulo.v
src/Util/ZUtil/Modulo.vo (real: 7.61, user: 7.43, sys: 0.17, mem: 507944 ko)
COQC src/Util/ZUtil/Pow2Mod.v
src/Util/ZUtil/Pow2Mod.vo (real: 1.68, user: 1.51, sys: 0.16, mem: 464336 ko)
COQC src/Util/ZUtil/LandLorShiftBounds.v
src/Util/ZUtil/LandLorShiftBounds.vo (real: 4.13, user: 3.99, sys: 0.13, mem: 487152 ko)
COQC src/Util/ZUtil/OnesFrom.v
src/Util/ZUtil/OnesFrom.vo (real: 1.28, user: 1.11, sys: 0.16, mem: 464080 ko)
COQC src/Util/ZUtil/TwosComplement.v
src/Util/ZUtil/TwosComplement.vo (real: 2.43, user: 2.25, sys: 0.17, mem: 472244 ko)
COQC src/Arithmetic/BarrettReduction/Wikipedia.v
src/Arithmetic/BarrettReduction/Wikipedia.vo (real: 1.09, user: 0.90, sys: 0.19, mem: 469888 ko)
COQC src/CastLemmas.v
src/CastLemmas.vo (real: 4.58, user: 4.37, sys: 0.20, mem: 509740 ko)
COQC src/Rewriter/TestRulesProofs.v
src/Rewriter/TestRulesProofs.vo (real: 0.63, user: 0.47, sys: 0.16, mem: 469980 ko)
COQC src/Arithmetic/BarrettReduction/HAC.v
src/Arithmetic/BarrettReduction/HAC.vo (real: 3.92, user: 3.75, sys: 0.16, mem: 486340 ko)
COQC src/Util/ZUtil/Tactics.v
src/Util/ZUtil/Tactics.vo (real: 0.56, user: 0.44, sys: 0.11, mem: 430812 ko)
COQC src/Util/ZUtil/Quot.v
src/Util/ZUtil/Quot.vo (real: 1.58, user: 1.43, sys: 0.14, mem: 475316 ko)
COQC src/Util/ZRange/SplitRangeBounds.v
src/Util/ZRange/SplitRangeBounds.vo (real: 1.78, user: 1.61, sys: 0.17, mem: 492412 ko)
COQC src/Util/ZUtil/Bitwise.v
src/Util/ZUtil/Bitwise.vo (real: 2.05, user: 1.90, sys: 0.14, mem: 486968 ko)
COQC src/Util/NumTheoryUtil.v
src/Util/NumTheoryUtil.vo (real: 1.01, user: 0.87, sys: 0.14, mem: 473464 ko)
COQC src/Util/ZUtil/EquivModulo.v
src/Util/ZUtil/EquivModulo.vo (real: 0.64, user: 0.48, sys: 0.15, mem: 461224 ko)
COQC src/Arithmetic/BarrettReduction/Generalized.v
src/Arithmetic/BarrettReduction/Generalized.vo (real: 9.38, user: 9.23, sys: 0.14, mem: 511396 ko)
COQC src/Util/ZUtil/TruncatingShiftl.v
src/Util/ZUtil/TruncatingShiftl.vo (real: 0.99, user: 0.85, sys: 0.14, mem: 466504 ko)
COQC src/Algebra/Field.v
src/Algebra/Field.vo (real: 16.51, user: 16.33, sys: 0.17, mem: 521972 ko)
COQC src/Util/ZUtil/Shift.v
src/Util/ZUtil/Shift.vo (real: 2.67, user: 2.50, sys: 0.16, mem: 479628 ko)
COQC src/Util/ZUtil/LandLorBounds.v
src/Util/ZUtil/LandLorBounds.vo (real: 3.97, user: 3.82, sys: 0.15, mem: 505228 ko)
COQC src/Util/ZUtil/Tactics/SolveRange.v
src/Util/ZUtil/Tactics/SolveRange.vo (real: 0.59, user: 0.48, sys: 0.10, mem: 464884 ko)
COQC src/Arithmetic/MontgomeryReduction/Definition.v
src/Arithmetic/MontgomeryReduction/Definition.vo (real: 0.52, user: 0.38, sys: 0.13, mem: 428832 ko)
COQC src/Util/ZRange/SplitBounds.v
src/Util/ZRange/SplitBounds.vo (real: 1.53, user: 1.40, sys: 0.13, mem: 484068 ko)
COQC src/Language/IdentifiersBasicGENERATED.v
Building index_of_base...
Building base_type_list...
Building eta_base_cps_gen...
Building eta_base_cps...
Building base_interp...
Building all_base...
Building all_base_and_interp...
Building index_of_ident...
Building ident_interp...
Building base_eq_dec...
Building base_beq_and_reflect...
Building base_beq...
Building reflect_base_beq...
Building baseHasNatAndCorrect...
Building baseHasNat...
Building baseHasNatCorrect...
Building base_interp_beq...
Building reflect_base_interp_beq...
Building try_make_base_transport_cps...
Building try_make_base_transport_cps_correct...
Building all_idents...
Building all_ident_and_interp...
Building buildEagerIdentAndInterpCorrect...
Building buildEagerIdent...
Building buildInterpEagerIdentCorrect...
Building toRestrictedIdentAndCorrect...
Building toRestrictedIdent...
Building toFromRestrictedIdent...
Building buildIdentAndInterpCorrect...
Building buildIdent...
Building buildInterpIdentCorrect...
Building ident_is_var_like...
Building eqv_Reflexive_Proper...
Building ident_interp_Proper...
Building invertIdent...
Building buildInvertIdentCorrect...
Building base_default...
Building package...
src/Language/IdentifiersBasicGENERATED.vo (real: 9.36, user: 9.12, sys: 0.23, mem: 639660 ko)
COQC src/Spec/MontgomeryCurve.v
src/Spec/MontgomeryCurve.vo (real: 2.92, user: 2.72, sys: 0.19, mem: 510380 ko)
COQC src/Algebra/Field_test.v
src/Algebra/Field_test.vo (real: 4.86, user: 4.69, sys: 0.17, mem: 542332 ko)
COQC src/Curves/Edwards/Pre.v
src/Curves/Edwards/Pre.vo (real: 5.99, user: 5.81, sys: 0.18, mem: 575804 ko)
COQC src/Spec/WeierstrassCurve.v
src/Spec/WeierstrassCurve.vo (real: 1.84, user: 1.71, sys: 0.12, mem: 482108 ko)
COQC src/Util/ZRange/CornersMonotoneBounds.v
src/Util/ZRange/CornersMonotoneBounds.vo (real: 9.28, user: 9.13, sys: 0.14, mem: 513516 ko)
COQC src/Arithmetic/ModularArithmeticPre.v
src/Arithmetic/ModularArithmeticPre.vo (real: 0.67, user: 0.55, sys: 0.12, mem: 469636 ko)
COQC src/Language/APINotations.v
src/Language/APINotations.vo (real: 1.46, user: 1.26, sys: 0.19, mem: 559640 ko)
COQC src/Util/FsatzAutoLemmas.v
src/Util/FsatzAutoLemmas.vo (real: 5.70, user: 5.51, sys: 0.18, mem: 516824 ko)
COQC src/Util/ZUtil/SignBit.v
src/Util/ZUtil/SignBit.vo (real: 0.71, user: 0.57, sys: 0.13, mem: 469508 ko)
COQC src/Util/ZUtil/Morphisms.v
src/Util/ZUtil/Morphisms.vo (real: 4.70, user: 4.50, sys: 0.20, mem: 541012 ko)
COQC src/Spec/CompleteEdwardsCurve.v
src/Spec/CompleteEdwardsCurve.vo (real: 0.68, user: 0.53, sys: 0.14, mem: 458488 ko)
COQC src/Arithmetic/MontgomeryReduction/Proofs.v
src/Arithmetic/MontgomeryReduction/Proofs.vo (real: 5.61, user: 5.44, sys: 0.17, mem: 486816 ko)
COQC src/Curves/Weierstrass/Affine.v
src/Curves/Weierstrass/Affine.vo (real: 0.67, user: 0.50, sys: 0.17, mem: 457772 ko)
COQC src/Curves/Montgomery/Affine.v
src/Curves/Montgomery/Affine.vo (real: 4.60, user: 4.42, sys: 0.17, mem: 552900 ko)
COQC src/Assembly/Parse/TestAsm.v
Finished transaction in 1.467 secs (0.413u,0.035s) (successful)
Finished transaction in 0.465 secs (0.344u,0.056s) (successful)
Finished transaction in 0.438 secs (0.318u,0.052s) (successful)
Finished transaction in 1.278 secs (1.142u,0.068s) (successful)
Finished transaction in 3.903 secs (3.775u,0.047s) (successful)
Finished transaction in 2.43 secs (2.289u,0.064s) (successful)
Finished transaction in 2.687 secs (2.559u,0.055s) (successful)
Finished transaction in 5.573 secs (5.416u,0.08s) (successful)
Finished transaction in 3.865 secs (3.734u,0.055s) (successful)
src/Assembly/Parse/TestAsm.vo (real: 29.94, user: 28.65, sys: 1.27, mem: 1004604 ko)
COQC src/Primitives/MxDHRepChange.v
src/Primitives/MxDHRepChange.vo (real: 12.54, user: 12.35, sys: 0.19, mem: 541576 ko)
COQC src/Util/ZUtil.v
src/Util/ZUtil.vo (real: 0.65, user: 0.47, sys: 0.18, mem: 487360 ko)
COQC src/Spec/ModularArithmetic.v
src/Spec/ModularArithmetic.vo (real: 0.57, user: 0.40, sys: 0.16, mem: 441464 ko)
COQC src/Language/API.v
src/Language/API.vo (real: 1.28, user: 1.08, sys: 0.19, mem: 552128 ko)
COQC src/Util/QUtil.v
src/Util/QUtil.vo (real: 0.96, user: 0.78, sys: 0.17, mem: 488636 ko)
COQC src/Language/IdentifiersGENERATED.v
Building all_base...
Building all_idents...
Building ident_index...
Building eta_ident_cps_gen...
Building eta_ident_cps_gen_expand_literal...
Building eta_ident_cps...
Building simple_idents...
Building all_raw_idents...
Building raw_ident_index...
Building raw_ident_index_idempotent...
Building eta_raw_ident_cps_gen...
Building raw_ident_to_ident...
Building raw_ident_infos_of...
Building split_raw_ident_gen...
Building invert_bind_args...
Building invert_bind_args_unknown...
Building all_pattern_idents...
Building eta_pattern_ident_cps_gen...
Building eta_pattern_ident_cps_gen_expand_literal...
Building split_types...
Building add_types_from_raw_sig...
Building to_type_split_types_subst_default_eq...
Building projT1_add_types_from_raw_sig_eq...
Building arg_types_unfolded...
Building type_of_list_arg_types_beq_unfolded...
Building to_typed_unfolded...
Building of_typed_ident_unfolded...
Building arg_types_of_typed_ident_unfolded...
Building unify...
Building unify_unknown...
Building final ident package...
Finished transaction in 17.006 secs (16.952u,0.036s) (successful)
src/Language/IdentifiersGENERATED.vo (real: 19.07, user: 18.81, sys: 0.23, mem: 748044 ko)
COQC src/PushButtonSynthesis/ReificationCache.v
src/PushButtonSynthesis/ReificationCache.vo (real: 1.34, user: 1.16, sys: 0.17, mem: 557388 ko)
COQC src/Arithmetic/Primitives.v
src/Arithmetic/Primitives.vo (real: 2.79, user: 2.59, sys: 0.18, mem: 479256 ko)
COQC src/Util/ZRange/LandLorBounds.v
src/Util/ZRange/LandLorBounds.vo (real: 16.91, user: 16.69, sys: 0.20, mem: 686216 ko)
COQC src/Util/ZUtil/ArithmeticShiftr.v
src/Util/ZUtil/ArithmeticShiftr.vo (real: 26.22, user: 26.00, sys: 0.21, mem: 670292 ko)
COQC src/Curves/Edwards/AffineProofs.v
src/Curves/Edwards/AffineProofs.vo (real: 27.40, user: 24.90, sys: 0.27, mem: 805908 ko)
COQC src/Curves/Montgomery/XZ.v
src/Curves/Montgomery/XZ.vo (real: 0.84, user: 0.50, sys: 0.17, mem: 462380 ko)
COQC src/Demo.v
src/Demo.vo (real: 60.68, user: 54.90, sys: 0.21, mem: 648712 ko)
COQC src/Curves/Weierstrass/Jacobian.v
Finished transaction in 18.02 secs (17.246u,0.019s) (successful)
Finished transaction in 6.464 secs (6.443u,0.02s) (successful)
Finished transaction in 1.434 secs (1.434u,0.s) (successful)
src/Curves/Weierstrass/Jacobian.vo (real: 84.62, user: 80.07, sys: 0.30, mem: 1168340 ko)
COQC src/AbstractInterpretation/ZRange.v
src/AbstractInterpretation/ZRange.vo (real: 2.14, user: 1.98, sys: 0.15, mem: 583324 ko)
COQC src/Language/InversionExtra.v
src/Language/InversionExtra.vo (real: 5.85, user: 5.39, sys: 0.17, mem: 608452 ko)
COQC src/Arithmetic/ModularArithmeticTheorems.v
src/Arithmetic/ModularArithmeticTheorems.vo (real: 2.44, user: 2.07, sys: 0.15, mem: 513032 ko)
COQC src/Language/WfExtra.v
src/Language/WfExtra.vo (real: 1.57, user: 1.15, sys: 0.14, mem: 553972 ko)
COQC src/Language/IdentifiersGENERATEDProofs.v
Proving is_simple_correct0...
Tactic call ran for 1.413 secs (1.268u,0.004s) (success)
Proving invert_bind_args_raw_to_typed...
Tactic call ran for 0.531 secs (0.518u,0.s) (success)
Proving fold_invert_bind_args...
Tactic call ran for 0.465 secs (0.443u,0.s) (success)
Proving split_ident_to_ident...
Tactic call ran for 0.162 secs (0.162u,0.s) (success)
Proving eq_indep_types_of_eq_types...
Tactic call ran for 1.462 secs (1.322u,0.007s) (success)
Proving fold_eta_ident_cps...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving fold_unify...
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving to_typed_of_typed_ident...
Tactic call ran for 2.393 secs (1.842u,0.003s) (success)
Proving eq_invert_bind_args_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
Proving eq_unify_unknown...
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
src/Language/IdentifiersGENERATEDProofs.vo (real: 18.09, user: 16.27, sys: 0.20, mem: 649668 ko)
COQC src/Util/ZRange/OperationsBounds.v
src/Util/ZRange/OperationsBounds.vo (real: 0.91, user: 0.77, sys: 0.14, mem: 477548 ko)
COQC src/Curves/Weierstrass/Projective.v
src/Curves/Weierstrass/Projective.vo (real: 163.57, user: 219.47, sys: 1.81, mem: 1300204 ko)
COQC src/Arithmetic/PrimeFieldTheorems.v
src/Arithmetic/PrimeFieldTheorems.vo (real: 1.95, user: 1.76, sys: 0.18, mem: 546892 ko)
COQC src/ArithmeticCPS/Core.v
src/ArithmeticCPS/Core.vo (real: 0.88, user: 0.73, sys: 0.15, mem: 493804 ko)
COQC src/Spec/Test/X25519.v
src/Spec/Test/X25519.vo (real: 106.68, user: 103.87, sys: 0.19, mem: 571692 ko)
COQC src/Stringification/Language.v
src/Stringification/Language.vo (real: 2.74, user: 2.52, sys: 0.21, mem: 613536 ko)
COQC src/Curves/Edwards/XYZT/Basic.v
src/Curves/Edwards/XYZT/Basic.vo (real: 18.77, user: 19.81, sys: 0.67, mem: 828980 ko)
COQC src/AbstractInterpretation/AbstractInterpretation.v
src/AbstractInterpretation/AbstractInterpretation.vo (real: 2.19, user: 2.00, sys: 0.18, mem: 566928 ko)
COQC src/Language/UnderLetsProofsExtra.v
src/Language/UnderLetsProofsExtra.vo (real: 1.26, user: 1.07, sys: 0.17, mem: 554232 ko)
COQC src/MiscCompilerPassesProofsExtra.v
src/MiscCompilerPassesProofsExtra.vo (real: 1.35, user: 1.15, sys: 0.18, mem: 553076 ko)
COQC src/Rewriter/AllTacticsExtra.v
src/Rewriter/AllTacticsExtra.vo (real: 1.22, user: 1.02, sys: 0.18, mem: 560652 ko)
COQC src/AbstractInterpretation/ZRangeProofs.v
Finished transaction in 24.078 secs (24.053u,0.023s) (successful)
Finished transaction in 15.424 secs (14.937u,0.028s) (successful)
src/AbstractInterpretation/ZRangeProofs.vo (real: 84.02, user: 83.19, sys: 0.33, mem: 881068 ko)
COQC src/Arithmetic/Core.v
src/Arithmetic/Core.vo (real: 19.25, user: 18.88, sys: 0.15, mem: 571076 ko)
COQC src/Stringification/IR.v
src/Stringification/IR.vo (real: 17.93, user: 17.55, sys: 0.20, mem: 659020 ko)
COQC src/ArithmeticCPS/ModOps.v
src/ArithmeticCPS/ModOps.vo (real: 0.97, user: 0.77, sys: 0.17, mem: 503524 ko)
COQC src/Curves/Edwards/XYZT/Precomputed.v
src/Curves/Edwards/XYZT/Precomputed.vo (real: 1.58, user: 1.38, sys: 0.18, mem: 493796 ko)
COQC src/Rewriter/Passes/Test.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.022 secs (0.022u,0.s) (success)
Tactic call ran for 0.207 secs (0.194u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.491 secs (0.486u,0.003s) (success)
Tactic call ran for 0.07 secs (0.07u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/Test.vo (real: 3.72, user: 3.48, sys: 0.20, mem: 584112 ko)
COQC src/Assembly/Equivalence.v
src/Assembly/Equivalence.vo (real: 1.89, user: 1.67, sys: 0.19, mem: 599344 ko)
COQC src/Arithmetic/ModOps.v
src/Arithmetic/ModOps.vo (real: 2.23, user: 2.05, sys: 0.16, mem: 533944 ko)
COQC src/Arithmetic/Partition.v
src/Arithmetic/Partition.vo (real: 1.63, user: 1.40, sys: 0.20, mem: 512592 ko)
COQC src/Stringification/C.v
src/Stringification/C.vo (real: 1.76, user: 1.57, sys: 0.17, mem: 579564 ko)
COQC src/Stringification/Rust.v
src/Stringification/Rust.vo (real: 1.66, user: 1.49, sys: 0.15, mem: 575660 ko)
COQC src/Stringification/Go.v
src/Stringification/Go.vo (real: 2.03, user: 1.85, sys: 0.17, mem: 580568 ko)
COQC src/Stringification/Java.v
src/Stringification/Java.vo (real: 1.77, user: 1.56, sys: 0.21, mem: 576172 ko)
COQC src/Stringification/JSON.v
src/Stringification/JSON.vo (real: 1.90, user: 1.68, sys: 0.21, mem: 579580 ko)
COQC src/Stringification/Zig.v
src/Stringification/Zig.vo (real: 1.81, user: 1.59, sys: 0.21, mem: 576892 ko)
COQC src/ArithmeticCPS/Saturated.v
src/ArithmeticCPS/Saturated.vo (real: 0.89, user: 0.73, sys: 0.16, mem: 491652 ko)
COQC src/Rewriter/RulesProofs.v
Finished transaction in 0.304 secs (0.304u,0.s) (successful)
Finished transaction in 0.018 secs (0.018u,0.s) (successful)
Finished transaction in 13.242 secs (13.119u,0.s) (successful)
Finished transaction in 0.171 secs (0.171u,0.s) (successful)
src/Rewriter/RulesProofs.vo (real: 62.51, user: 61.74, sys: 0.21, mem: 773632 ko)
COQC src/Arithmetic/UniformWeight.v
src/Arithmetic/UniformWeight.vo (real: 4.31, user: 4.14, sys: 0.16, mem: 535376 ko)
COQC src/UnsaturatedSolinasHeuristics.v
src/UnsaturatedSolinasHeuristics.vo (real: 5.38, user: 5.21, sys: 0.17, mem: 543176 ko)
COQC src/ArithmeticCPS/BaseConversion.v
src/ArithmeticCPS/BaseConversion.vo (real: 0.90, user: 0.74, sys: 0.15, mem: 503480 ko)
COQC src/Fancy/Compiler.v
src/Fancy/Compiler.vo (real: 224.06, user: 216.92, sys: 0.38, mem: 1259636 ko)
COQC src/Arithmetic/Saturated.v
src/Arithmetic/Saturated.vo (real: 34.60, user: 34.25, sys: 0.30, mem: 569628 ko)
COQC src/Rewriter/Passes/AddAssocLeft.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.035 secs (0.035u,0.s) (success)
Tactic call ran for 0.01 secs (0.01u,0.s) (success)
Tactic call ran for 0.078 secs (0.078u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.016 secs (0.016u,0.s) (success)
Tactic call ran for 0.259 secs (0.259u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.342 secs (0.342u,0.s) (success)
Tactic call ran for 0.064 secs (0.064u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/AddAssocLeft.vo (real: 3.59, user: 3.34, sys: 0.24, mem: 605072 ko)
COQC src/UnsaturatedSolinasHeuristics/Tests.v
Finished transaction in 40.862 secs (40.345u,0.052s) (successful)
Finished transaction in 31.323 secs (30.905u,0.131s) (successful)
src/UnsaturatedSolinasHeuristics/Tests.vo (real: 77.43, user: 76.81, sys: 0.56, mem: 1132364 ko)
COQC src/Rewriter/Passes/Arith.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.796 secs (0.792u,0.004s) (success)
Tactic call ran for 22.413 secs (22.325u,0.088s) (success)
Tactic call ran for 0.212 secs (0.212u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.642 secs (0.642u,0.s) (success)
Tactic call ran for 4.196 secs (4.196u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 6.767 secs (6.767u,0.s) (success)
Tactic call ran for 1.33 secs (1.33u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/Arith.vo (real: 58.93, user: 58.57, sys: 0.35, mem: 1057304 ko)
COQC src/Rewriter/Passes/StripLiteralCasts.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.027 secs (0.027u,0.s) (success)
Tactic call ran for 0.003 secs (0.003u,0.s) (success)
Tactic call ran for 0.069 secs (0.069u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.012 secs (0.012u,0.s) (success)
Tactic call ran for 0.01 secs (0.01u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.196 secs (0.196u,0.s) (success)
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/StripLiteralCasts.vo (real: 2.50, user: 2.31, sys: 0.18, mem: 593588 ko)
COQC src/Rewriter/Passes/FlattenThunkedRects.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.036 secs (0.036u,0.s) (success)
Tactic call ran for 0.008 secs (0.008u,0.s) (success)
Tactic call ran for 0.08 secs (0.08u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.015 secs (0.015u,0.s) (success)
Tactic call ran for 0.14 secs (0.14u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.251 secs (0.251u,0.s) (success)
Tactic call ran for 0.045 secs (0.045u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/FlattenThunkedRects.vo (real: 3.12, user: 2.92, sys: 0.20, mem: 598576 ko)
COQC src/AbstractInterpretation/Wf.v
src/AbstractInterpretation/Wf.vo (real: 151.88, user: 151.45, sys: 0.37, mem: 962280 ko)
COQC src/Curves/Weierstrass/AffineProofs.v
Finished transaction in 1.655 secs (1.65u,0.004s) (successful)
Finished transaction in 306.899 secs (91.391u,0.584s) (successful)
Finished transaction in 38.894 secs (38.912u,0.s) (successful)
src/Curves/Weierstrass/AffineProofs.vo (real: 348.25, user: 547.58, sys: 2.03, mem: 2416924 ko)
COQC src/Rewriter/Passes/NoSelect.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.049 secs (0.049u,0.s) (success)
Tactic call ran for 0.014 secs (0.014u,0.s) (success)
Tactic call ran for 0.082 secs (0.082u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.034 secs (0.03u,0.003s) (success)
Tactic call ran for 0.45 secs (0.438u,0.011s) (success)
Proving Rewriter_Interp...
Tactic call ran for 1.419 secs (1.419u,0.s) (success)
Tactic call ran for 0.777 secs (0.773u,0.004s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/NoSelect.vo (real: 8.05, user: 7.80, sys: 0.24, mem: 641564 ko)
COQC src/Rewriter/Passes/ToFancy.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.018 secs (0.018u,0.s) (success)
Tactic call ran for 0.006 secs (0.006u,0.s) (success)
Tactic call ran for 0.072 secs (0.072u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.012 secs (0.012u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.124 secs (0.124u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/ToFancy.vo (real: 2.28, user: 2.09, sys: 0.19, mem: 593380 ko)
COQC src/Rewriter/Passes/MulSplit.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.248 secs (0.248u,0.s) (success)
Tactic call ran for 0.709 secs (0.705u,0.004s) (success)
Tactic call ran for 0.118 secs (0.118u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.317 secs (0.317u,0.s) (success)
Tactic call ran for 2.946 secs (2.938u,0.007s) (success)
Proving Rewriter_Interp...
Tactic call ran for 9.625 secs (9.617u,0.007s) (success)
Tactic call ran for 4.565 secs (4.545u,0.02s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/MulSplit.vo (real: 42.25, user: 42.00, sys: 0.24, mem: 882088 ko)
COQC src/Rewriter/Passes/UnfoldValueBarrier.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.023 secs (0.023u,0.s) (success)
Tactic call ran for 0.003 secs (0.003u,0.s) (success)
Tactic call ran for 0.069 secs (0.069u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.013 secs (0.013u,0.s) (success)
Tactic call ran for 0.039 secs (0.039u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 0.163 secs (0.163u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/UnfoldValueBarrier.vo (real: 2.53, user: 2.33, sys: 0.20, mem: 595564 ko)
COQC src/AbstractInterpretation/WfExtra.v
src/AbstractInterpretation/WfExtra.vo (real: 1.34, user: 1.15, sys: 0.18, mem: 559816 ko)
COQC src/Rewriter/Passes/MultiRetSplit.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 0.271 secs (0.266u,0.003s) (success)
Tactic call ran for 1.699 secs (1.69u,0.007s) (success)
Tactic call ran for 0.145 secs (0.145u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 0.521 secs (0.513u,0.007s) (success)
Tactic call ran for 5. secs (4.982u,0.012s) (success)
Proving Rewriter_Interp...
Tactic call ran for 14.168 secs (14.124u,0.015s) (success)
Tactic call ran for 8.637 secs (8.599u,0.027s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/MultiRetSplit.vo (real: 70.82, user: 70.37, sys: 0.36, mem: 1105200 ko)
COQC src/Arithmetic/BaseConversion.v
src/Arithmetic/BaseConversion.vo (real: 2.42, user: 2.26, sys: 0.15, mem: 526700 ko)
COQC src/PushButtonSynthesis/SaturatedSolinasReificationCache.v
Finished transaction in 3.887 secs (3.867u,0.019s) (successful)
Finished transaction in 1.574 secs (1.574u,0.s) (successful)
src/PushButtonSynthesis/SaturatedSolinasReificationCache.vo (real: 7.33, user: 7.09, sys: 0.23, mem: 651252 ko)
COQC src/PushButtonSynthesis/BaseConversionReificationCache.v
Finished transaction in 1.602 secs (1.59u,0.012s) (successful)
Finished transaction in 0.602 secs (0.602u,0.s) (successful)
src/PushButtonSynthesis/BaseConversionReificationCache.vo (real: 3.76, user: 3.57, sys: 0.19, mem: 618260 ko)
COQC src/ArithmeticCPS/Freeze.v
src/ArithmeticCPS/Freeze.vo (real: 1.02, user: 0.85, sys: 0.16, mem: 509152 ko)
COQC src/Arithmetic/BarrettReduction.v
src/Arithmetic/BarrettReduction.vo (real: 21.76, user: 21.56, sys: 0.20, mem: 606060 ko)
COQC src/Rewriter/Passes/NBE.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 2.125 secs (2.125u,0.s) (success)
Tactic call ran for 128.961 secs (128.852u,0.107s) (success)
Tactic call ran for 0.406 secs (0.406u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 2.032 secs (2.032u,0.s) (success)
Tactic call ran for 3.177 secs (3.177u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 9.73 secs (9.73u,0.s) (success)
Tactic call ran for 5.354 secs (5.354u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/NBE.vo (real: 193.43, user: 193.00, sys: 0.43, mem: 1444416 ko)
COQC src/Arithmetic/FancyMontgomeryReduction.v
src/Arithmetic/FancyMontgomeryReduction.vo (real: 11.86, user: 11.69, sys: 0.17, mem: 561500 ko)
COQC src/AbstractInterpretation/Proofs.v
src/AbstractInterpretation/Proofs.vo (real: 78.50, user: 78.24, sys: 0.25, mem: 789636 ko)
COQC src/Fancy/Prod.v
src/Fancy/Prod.vo (real: 6.05, user: 5.85, sys: 0.19, mem: 622804 ko)
COQC src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
Finished transaction in 11.932 secs (11.879u,0.052s) (successful)
Finished transaction in 4.019 secs (4.019u,0.s) (successful)
src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo (real: 18.10, user: 17.86, sys: 0.23, mem: 763788 ko)
COQC src/Arithmetic/Freeze.v
src/Arithmetic/Freeze.vo (real: 2.74, user: 2.57, sys: 0.16, mem: 542176 ko)
COQC src/ArithmeticCPS/WordByWordMontgomery.v
src/ArithmeticCPS/WordByWordMontgomery.vo (real: 0.97, user: 0.82, sys: 0.15, mem: 507064 ko)
COQC src/PushButtonSynthesis/BarrettReductionReificationCache.v
Finished transaction in 19.122 secs (19.029u,0.091s) (successful)
Finished transaction in 6.865 secs (6.862u,0.s) (successful)
src/PushButtonSynthesis/BarrettReductionReificationCache.vo (real: 31.84, user: 31.55, sys: 0.29, mem: 899464 ko)
COQC src/Arithmetic/WordByWordMontgomery.v
src/Arithmetic/WordByWordMontgomery.vo (real: 22.07, user: 21.83, sys: 0.22, mem: 649836 ko)
COQC src/Arithmetic/BYInv.v
src/Arithmetic/BYInv.vo (real: 7.65, user: 7.44, sys: 0.21, mem: 631712 ko)
COQC src/Rewriter/Passes/ToFancyWithCasts.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 1.193 secs (1.189u,0.003s) (success)
Tactic call ran for 48.356 secs (48.232u,0.123s) (success)
Tactic call ran for 0.399 secs (0.399u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 1.571 secs (1.571u,0.s) (success)
Tactic call ran for 7.831 secs (7.817u,0.011s) (success)
Proving Rewriter_Interp...
Tactic call ran for 26.748 secs (26.526u,0.016s) (success)
Tactic call ran for 6.893 secs (6.828u,0.003s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/ToFancyWithCasts.vo (real: 158.59, user: 157.55, sys: 0.58, mem: 1481732 ko)
COQC src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
Finished transaction in 3.024 secs (3.008u,0.015s) (successful)
Finished transaction in 1.259 secs (1.255u,0.003s) (successful)
Finished transaction in 5.027 secs (5.019u,0.007s) (successful)
Finished transaction in 1.859 secs (1.855u,0.003s) (successful)
Finished transaction in 5.259 secs (5.251u,0.007s) (successful)
Finished transaction in 2.264 secs (2.264u,0.s) (successful)
Finished transaction in 1.787 secs (1.775u,0.011s) (successful)
Finished transaction in 0.735 secs (0.735u,0.s) (successful)
Finished transaction in 2.241 secs (2.237u,0.003s) (successful)
Finished transaction in 0.834 secs (0.834u,0.s) (successful)
Finished transaction in 0.522 secs (0.522u,0.s) (successful)
Finished transaction in 0.212 secs (0.212u,0.s) (successful)
Finished transaction in 1.647 secs (1.634u,0.011s) (successful)
Finished transaction in 0.623 secs (0.623u,0.s) (successful)
Finished transaction in 1.769 secs (1.761u,0.008s) (successful)
Finished transaction in 0.591 secs (0.591u,0.s) (successful)
Finished transaction in 2.321 secs (2.321u,0.s) (successful)
Finished transaction in 0.738 secs (0.738u,0.s) (successful)
Finished transaction in 2.346 secs (2.345u,0.s) (successful)
Finished transaction in 0.813 secs (0.813u,0.s) (successful)
Finished transaction in 2.488 secs (2.488u,0.s) (successful)
Finished transaction in 0.804 secs (0.804u,0.s) (successful)
Finished transaction in 0.193 secs (0.193u,0.s) (successful)
Finished transaction in 0.078 secs (0.078u,0.s) (successful)
Finished transaction in 0.226 secs (0.226u,0.s) (successful)
Finished transaction in 0.065 secs (0.065u,0.s) (successful)
Finished transaction in 3.769 secs (3.749u,0.019s) (successful)
Finished transaction in 1.379 secs (1.379u,0.s) (successful)
Finished transaction in 1.546 secs (1.546u,0.s) (successful)
Finished transaction in 0.519 secs (0.519u,0.s) (successful)
src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo (real: 52.74, user: 52.38, sys: 0.35, mem: 963324 ko)
COQC src/COperationSpecifications.v
src/COperationSpecifications.vo (real: 6.01, user: 5.82, sys: 0.19, mem: 596512 ko)
COQC src/Curves/Montgomery/AffineProofs.v
Finished transaction in 0.6 secs (0.6u,0.s) (successful)
Finished transaction in 102.776 secs (15.668u,0.227s) (successful)
src/Curves/Montgomery/AffineProofs.vo (real: 108.54, user: 192.73, sys: 1.38, mem: 1252056 ko)
COQC src/Curves/Montgomery/AffineInstances.v
src/Curves/Montgomery/AffineInstances.vo (real: 1.29, user: 1.11, sys: 0.17, mem: 479672 ko)
COQC src/Rewriter/Passes/ArithWithCasts.v
Reifying...
Compiling decision tree...
Splitting rewrite rules...
Assembling rewrite_head...
Reducing rewrite_head...
Tactic call ran for 1.303 secs (1.299u,0.003s) (success)
Tactic call ran for 117.631 secs (117.503u,0.099s) (success)
Tactic call ran for 0.261 secs (0.261u,0.s) (success)
Assembling rewrite_head_no_dtree...
Reducing rewrite_head_no_dtree...
Proving Rewriter_Wf...
Tactic call ran for 2.294 secs (2.291u,0.s) (success)
Tactic call ran for 8.886 secs (8.843u,0.s) (success)
Proving Rewriter_Interp...
Tactic call ran for 25.485 secs (25.484u,0.s) (success)
Tactic call ran for 9.682 secs (9.682u,0.s) (success)
Assembling verified rewriter...
Refining with verified rewriter...
src/Rewriter/Passes/ArithWithCasts.vo (real: 239.79, user: 239.26, sys: 0.45, mem: 1608244 ko)
COQC src/PushButtonSynthesis/BYInversionReificationCache.v
Finished transaction in 18.424 secs (18.254u,0.116s) (successful)
Finished transaction in 5.578 secs (5.57u,0.008s) (successful)
Finished transaction in 0.133 secs (0.133u,0.s) (successful)
Finished transaction in 0.044 secs (0.044u,0.s) (successful)
Finished transaction in 0.315 secs (0.311u,0.003s) (successful)
Finished transaction in 0.099 secs (0.099u,0.s) (successful)
src/PushButtonSynthesis/BYInversionReificationCache.vo (real: 33.80, user: 33.35, sys: 0.38, mem: 1033764 ko)
COQC src/Rewriter/All.v
src/Rewriter/All.vo (real: 1.39, user: 1.22, sys: 0.16, mem: 615916 ko)
COQC src/CompilersTestCases.v
src/CompilersTestCases.vo (real: 2.42, user: 2.17, sys: 0.25, mem: 647496 ko)
COQC src/BoundsPipeline.v
src/BoundsPipeline.vo (real: 6.25, user: 6.00, sys: 0.25, mem: 709228 ko)
COQC src/PushButtonSynthesis/Primitives.v
Finished transaction in 0.016 secs (0.016u,0.s) (successful)
Finished transaction in 0.004 secs (0.004u,0.s) (successful)
Finished transaction in 0.068 secs (0.068u,0.s) (successful)
Finished transaction in 0.045 secs (0.045u,0.s) (successful)
Finished transaction in 0.151 secs (0.151u,0.s) (successful)
Finished transaction in 0.054 secs (0.054u,0.s) (successful)
Finished transaction in 0.07 secs (0.07u,0.s) (successful)
Finished transaction in 0.033 secs (0.033u,0.s) (successful)
Finished transaction in 0.084 secs (0.084u,0.s) (successful)
Finished transaction in 0.034 secs (0.034u,0.s) (successful)
Finished transaction in 0.008 secs (0.008u,0.s) (successful)
Finished transaction in 0.003 secs (0.003u,0.s) (successful)
Finished transaction in 0.095 secs (0.095u,0.s) (successful)
Finished transaction in 0.037 secs (0.037u,0.s) (successful)
Finished transaction in 0.088 secs (0.088u,0.s) (successful)
Finished transaction in 0.033 secs (0.033u,0.s) (successful)
src/PushButtonSynthesis/Primitives.vo (real: 7.79, user: 7.51, sys: 0.27, mem: 814480 ko)
COQC src/PushButtonSynthesis/SmallExamples.v
Finished transaction in 1.273 secs (1.269u,0.004s) (successful)
Finished transaction in 1.946 secs (1.941u,0.004s) (successful)
Finished transaction in 0.121 secs (0.12u,0.s) (successful)
Finished transaction in 0.574 secs (0.573u,0.s) (successful)
Finished transaction in 3.41 secs (3.401u,0.007s) (successful)
Finished transaction in 0.182 secs (0.182u,0.s) (successful)
Finished transaction in 0.101 secs (0.1u,0.s) (successful)
Finished transaction in 0.096 secs (0.095u,0.s) (successful)
Finished transaction in 0.112 secs (0.111u,0.s) (successful)
Finished transaction in 0.108 secs (0.107u,0.s) (successful)
Finished transaction in 0.118 secs (0.117u,0.s) (successful)
src/PushButtonSynthesis/SmallExamples.vo (real: 10.24, user: 9.98, sys: 0.24, mem: 780540 ko)
COQC src/PushButtonSynthesis/SaturatedSolinas.v
src/PushButtonSynthesis/SaturatedSolinas.vo (real: 4.43, user: 4.14, sys: 0.26, mem: 774888 ko)
COQC src/PushButtonSynthesis/BaseConversion.v
src/PushButtonSynthesis/BaseConversion.vo (real: 9.38, user: 9.14, sys: 0.23, mem: 793540 ko)
COQC src/PushButtonSynthesis/BarrettReduction.v
src/PushButtonSynthesis/BarrettReduction.vo (real: 7.46, user: 7.11, sys: 0.28, mem: 784340 ko)
COQC src/PushButtonSynthesis/FancyMontgomeryReduction.v
src/PushButtonSynthesis/FancyMontgomeryReduction.vo (real: 4.57, user: 4.29, sys: 0.27, mem: 786004 ko)
COQC src/PushButtonSynthesis/UnsaturatedSolinas.v
src/PushButtonSynthesis/UnsaturatedSolinas.vo (real: 26.69, user: 26.20, sys: 0.30, mem: 907280 ko)
COQC src/Fancy/Montgomery256.v
Finished transaction in 10.023 secs (9.991u,0.032s) (successful)
src/Fancy/Montgomery256.vo (real: 71.48, user: 71.08, sys: 0.39, mem: 1312400 ko)
COQC src/Fancy/Barrett256.v
Finished transaction in 28.222 secs (28.186u,0.036s) (successful)
src/Fancy/Barrett256.vo (real: 111.93, user: 111.43, sys: 0.43, mem: 1541516 ko)
DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions
DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256
DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct
DIFF Crypto.Fancy.Montgomery256.montred256
DIFF Crypto.Fancy.Barrett256.Prod.MulMod
DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct
DIFF Crypto.Fancy.Barrett256.barrett_red256
DIFF Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs
DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions
DIFF Crypto.UnsaturatedSolinasHeuristics.Tests.get_balances
COQC src/Curves/Montgomery/XZProofs.v
Finished transaction in 14.99 secs (14.97u,0.02s) (successful)
Finished transaction in 28.478 secs (7.178u,0.376s) (successful)
Finished transaction in 3.393 secs (3.392u,0.003s) (successful)
src/Curves/Montgomery/XZProofs.vo (real: 207.79, user: 228.45, sys: 1.38, mem: 2017408 ko)
COQC src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v
Finished transaction in 36.95 secs (36.389u,0.307s) (successful)
Finished transaction in 9.032 secs (9.007u,0.011s) (successful)
Finished transaction in 2.293 secs (2.279u,0.011s) (successful)
Finished transaction in 0.825 secs (0.824u,0.s) (successful)
Finished transaction in 2.213 secs (2.203u,0.007s) (successful)
Finished transaction in 0.764 secs (0.763u,0.s) (successful)
Finished transaction in 4.573 secs (4.544u,0.023s) (successful)
Finished transaction in 1.35 secs (1.344u,0.003s) (successful)
Finished transaction in 1.669 secs (1.655u,0.012s) (successful)
Finished transaction in 0.513 secs (0.513u,0.s) (successful)
Finished transaction in 1.618 secs (1.608u,0.007s) (successful)
Finished transaction in 0.566 secs (0.566u,0.s) (successful)
Finished transaction in 0.035 secs (0.035u,0.s) (successful)
Finished transaction in 0.011 secs (0.011u,0.s) (successful)
Finished transaction in 0.219 secs (0.215u,0.003s) (successful)
Finished transaction in 0.073 secs (0.073u,0.s) (successful)
Finished transaction in 0.249 secs (0.245u,0.003s) (successful)
Finished transaction in 0.074 secs (0.074u,0.s) (successful)
Finished transaction in 39.728 secs (39.633u,0.039s) (successful)
Finished transaction in 7.911 secs (7.895u,0.007s) (successful)
Finished transaction in 41.208 secs (41.161u,0.003s) (successful)
Finished transaction in 8.463 secs (8.445u,0.s) (successful)
Finished transaction in 35.16 secs (35.056u,0.055s) (successful)
Finished transaction in 7.796 secs (7.789u,0.s) (successful)
Finished transaction in 34.996 secs (34.936u,0.012s) (successful)
Finished transaction in 7.763 secs (7.747u,0.007s) (successful)
Finished transaction in 0.05 secs (0.05u,0.s) (successful)
Finished transaction in 0.021 secs (0.021u,0.s) (successful)
Finished transaction in 36.128 secs (36.013u,0.067s) (successful)
Finished transaction in 7.542 secs (7.531u,0.003s) (successful)
src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo (real: 298.95, user: 297.45, sys: 0.90, mem: 2020172 ko)
COQC src/PushButtonSynthesis/WordByWordMontgomery.v
src/PushButtonSynthesis/WordByWordMontgomery.vo (real: 26.20, user: 25.95, sys: 0.24, mem: 934280 ko)
COQC src/CLI.v
src/CLI.vo (real: 3.65, user: 3.39, sys: 0.25, mem: 791808 ko)
COQC src/StandaloneHaskellMain.v
src/StandaloneHaskellMain.vo (real: 2.48, user: 2.20, sys: 0.28, mem: 793264 ko)
COQC src/StandaloneOCamlMain.v
src/StandaloneOCamlMain.vo (real: 2.48, user: 2.22, sys: 0.26, mem: 793628 ko)
COQC src/ExtractionHaskell/saturated_solinas.v > src/ExtractionHaskell/saturated_solinas.hs
File "./src/ExtractionHaskell/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionHaskell/saturated_solinas.hs (real: 12.75, user: 12.26, sys: 0.45, mem: 1439060 ko)
COQC src/ExtractionHaskell/unsaturated_solinas.v > src/ExtractionHaskell/unsaturated_solinas.hs
File "./src/ExtractionHaskell/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionHaskell/unsaturated_solinas.hs (real: 13.74, user: 13.33, sys: 0.40, mem: 1497732 ko)
COQC src/ExtractionHaskell/word_by_word_montgomery.v > src/ExtractionHaskell/word_by_word_montgomery.hs
File "./src/ExtractionHaskell/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionHaskell/word_by_word_montgomery.hs (real: 18.73, user: 18.18, sys: 0.53, mem: 1870044 ko)
COQC src/ExtractionHaskell/base_conversion.v > src/ExtractionHaskell/base_conversion.hs
File "./src/ExtractionHaskell/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionHaskell/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionHaskell/base_conversion.hs (real: 11.90, user: 11.42, sys: 0.47, mem: 1410696 ko)
COQC src/ExtractionOCaml/unsaturated_solinas.v > src/ExtractionOCaml/unsaturated_solinas.ml
File "./src/ExtractionOCaml/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/unsaturated_solinas.v", line 3, characters 43-88:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionOCaml/unsaturated_solinas.ml (real: 23.52, user: 23.03, sys: 0.49, mem: 1653120 ko)
COQC src/ExtractionOCaml/saturated_solinas.v > src/ExtractionOCaml/saturated_solinas.ml
File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionOCaml/saturated_solinas.ml (real: 19.30, user: 18.72, sys: 0.57, mem: 1555312 ko)
COQC src/StandaloneDebuggingExamples.v
src/StandaloneDebuggingExamples.vo (real: 5.83, user: 5.55, sys: 0.27, mem: 858220 ko)
COQC src/ExtractionOCaml/base_conversion.v > src/ExtractionOCaml/base_conversion.ml
File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionOCaml/base_conversion.ml (real: 20.14, user: 19.66, sys: 0.47, mem: 1538868 ko)
COQC src/ExtractionOCaml/word_by_word_montgomery.v > src/ExtractionOCaml/word_by_word_montgomery.ml
File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
Warning: The identifier __ contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]
src/ExtractionOCaml/word_by_word_montgomery.ml (real: 37.76, user: 36.99, sys: 0.73, mem: 2284284 ko)
COQC src/Rewriter/PerfTesting/Core.v
Finished transaction in 25.318 secs (24.938u,0.379s) (successful)
Finished transaction in 39.562 secs (39.081u,0.479s) (successful)
src/Rewriter/PerfTesting/Core.vo (real: 69.92, user: 68.38, sys: 1.54, mem: 5393136 ko)
OCAMLOPT src/ExtractionOCaml/unsaturated_solinas.ml -o src/ExtractionOCaml/unsaturated_solinas
src/ExtractionOCaml/unsaturated_solinas (real: 34.69, user: 33.65, sys: 1.04, mem: 1212804 ko)
COQC src/Rewriter/PerfTesting/StandaloneOCamlMain.v
src/Rewriter/PerfTesting/StandaloneOCamlMain.vo (real: 2.93, user: 2.45, sys: 0.48, mem: 1323848 ko)
SYNTHESIZE > fiat-c/src/curve25519_64.c
fiat-c/src/curve25519_64.c (real: 0.52, user: 0.50, sys: 0.02, mem: 21024 ko)
SYNTHESIZE > fiat-c/src/curve25519_32.c
fiat-c/src/curve25519_32.c (real: 1.87, user: 1.82, sys: 0.04, mem: 24792 ko)
SYNTHESIZE > fiat-c/src/poly1305_64.c
fiat-c/src/poly1305_64.c (real: 0.16, user: 0.13, sys: 0.03, mem: 19424 ko)
SYNTHESIZE > fiat-c/src/poly1305_32.c
fiat-c/src/poly1305_32.c (real: 0.25, user: 0.23, sys: 0.02, mem: 19820 ko)
SYNTHESIZE > fiat-c/src/p521_64.c
fiat-c/src/p521_64.c (real: 3.31, user: 3.26, sys: 0.04, mem: 26128 ko)
COQC src/SlowPrimeSynthesisExamples.v
Finished transaction in 5.655 secs (5.639u,0.015s) (successful)
Finished transaction in 4.993 secs (4.973u,0.019s) (successful)
Finished transaction in 5.4 secs (5.4u,0.s) (successful)
Finished transaction in 5.164 secs (5.163u,0.s) (successful)
Finished transaction in 3.486 secs (3.478u,0.008s) (successful)
Finished transaction in 5.813 secs (5.797u,0.015s) (successful)
Finished transaction in 7.448 secs (7.447u,0.s) (successful)
Finished transaction in 5.328 secs (5.327u,0.s) (successful)
Finished transaction in 3.934 secs (3.933u,0.s) (successful)
Finished transaction in 2.235 secs (2.235u,0.s) (successful)
Finished transaction in 4.946 secs (4.941u,0.003s) (successful)
src/SlowPrimeSynthesisExamples.vo (real: 94.54, user: 94.08, sys: 0.44, mem: 1454884 ko)
OCAMLOPT src/ExtractionOCaml/saturated_solinas.ml -o src/ExtractionOCaml/saturated_solinas
src/ExtractionOCaml/saturated_solinas (real: 31.95, user: 30.83, sys: 1.11, mem: 1055052 ko)
SYNTHESIZE > fiat-c/src/p448_solinas_64.c
fiat-c/src/p448_solinas_64.c (real: 2.04, user: 1.99, sys: 0.04, mem: 25816 ko)
SYNTHESIZE > fiat-rust/src/curve25519_64.rs
fiat-rust/src/curve25519_64.rs (real: 0.52, user: 0.50, sys: 0.02, mem: 21056 ko)
SYNTHESIZE > fiat-rust/src/poly1305_64.rs
fiat-rust/src/poly1305_64.rs (real: 0.15, user: 0.12, sys: 0.02, mem: 19452 ko)
SYNTHESIZE > fiat-rust/src/poly1305_32.rs
fiat-rust/src/poly1305_32.rs (real: 0.25, user: 0.22, sys: 0.02, mem: 20080 ko)
SYNTHESIZE > fiat-rust/src/curve25519_32.rs
fiat-rust/src/curve25519_32.rs (real: 1.84, user: 1.78, sys: 0.05, mem: 24956 ko)
SYNTHESIZE > fiat-rust/src/p448_solinas_64.rs
fiat-rust/src/p448_solinas_64.rs (real: 2.05, user: 1.99, sys: 0.05, mem: 24856 ko)
SYNTHESIZE > fiat-rust/src/p521_64.rs
fiat-rust/src/p521_64.rs (real: 3.28, user: 3.22, sys: 0.05, mem: 26116 ko)
OCAMLOPT src/ExtractionOCaml/base_conversion.ml -o src/ExtractionOCaml/base_conversion
src/ExtractionOCaml/base_conversion (real: 31.87, user: 30.59, sys: 1.13, mem: 1055060 ko)
SYNTHESIZE > fiat-go/32/poly1305/poly1305.go
fiat-go/32/poly1305/poly1305.go (real: 0.23, user: 0.21, sys: 0.01, mem: 20068 ko)
SYNTHESIZE > fiat-go/64/curve25519/curve25519.go
fiat-go/64/curve25519/curve25519.go (real: 0.59, user: 0.56, sys: 0.02, mem: 23468 ko)
SYNTHESIZE > fiat-go/32/curve25519/curve25519.go
fiat-go/32/curve25519/curve25519.go (real: 1.82, user: 1.80, sys: 0.02, mem: 24904 ko)
SYNTHESIZE > fiat-go/64/poly1305/poly1305.go
fiat-go/64/poly1305/poly1305.go (real: 0.16, user: 0.15, sys: 0.01, mem: 19816 ko)
SYNTHESIZE > fiat-c/src/p448_solinas_32.c
fiat-c/src/p448_solinas_32.c (real: 7.83, user: 7.76, sys: 0.07, mem: 45388 ko)
SYNTHESIZE > fiat-json/src/curve25519_64.json
fiat-json/src/curve25519_64.json (real: 1.00, user: 0.95, sys: 0.04, mem: 23396 ko)
SYNTHESIZE > fiat-go/64/p448solinas/p448solinas.go
fiat-go/64/p448solinas/p448solinas.go (real: 2.21, user: 2.16, sys: 0.04, mem: 29324 ko)
SYNTHESIZE > fiat-json/src/poly1305_64.json
fiat-json/src/poly1305_64.json (real: 0.27, user: 0.25, sys: 0.02, mem: 20600 ko)
SYNTHESIZE > fiat-json/src/poly1305_32.json
fiat-json/src/poly1305_32.json (real: 0.51, user: 0.48, sys: 0.02, mem: 22504 ko)
SYNTHESIZE > fiat-go/64/p521/p521.go
fiat-go/64/p521/p521.go (real: 3.51, user: 3.46, sys: 0.05, mem: 31236 ko)
SYNTHESIZE > fiat-json/src/curve25519_32.json
fiat-json/src/curve25519_32.json (real: 4.68, user: 4.60, sys: 0.07, mem: 29948 ko)
SYNTHESIZE > fiat-rust/src/p448_solinas_32.rs
fiat-rust/src/p448_solinas_32.rs (real: 8.14, user: 8.05, sys: 0.08, mem: 45832 ko)
SYNTHESIZE > fiat-json/src/p448_solinas_64.json
fiat-json/src/p448_solinas_64.json (real: 4.28, user: 4.22, sys: 0.06, mem: 29948 ko)
SYNTHESIZE > fiat-java/src/FiatPoly1305.java
fiat-java/src/FiatPoly1305.java (real: 0.28, user: 0.25, sys: 0.02, mem: 20068 ko)
SYNTHESIZE > fiat-java/src/FiatCurve25519.java
fiat-java/src/FiatCurve25519.java (real: 1.92, user: 1.88, sys: 0.04, mem: 25044 ko)
SYNTHESIZE > fiat-zig/src/curve25519_64.zig
fiat-zig/src/curve25519_64.zig (real: 0.51, user: 0.48, sys: 0.03, mem: 21084 ko)
SYNTHESIZE > fiat-zig/src/poly1305_64.zig
fiat-zig/src/poly1305_64.zig (real: 0.15, user: 0.13, sys: 0.01, mem: 19236 ko)
SYNTHESIZE > fiat-json/src/p521_64.json
fiat-json/src/p521_64.json (real: 5.95, user: 5.88, sys: 0.06, mem: 28304 ko)
SYNTHESIZE > fiat-zig/src/poly1305_32.zig
fiat-zig/src/poly1305_32.zig (real: 0.25, user: 0.24, sys: 0.01, mem: 20504 ko)
SYNTHESIZE > fiat-zig/src/curve25519_32.zig
fiat-zig/src/curve25519_32.zig (real: 1.85, user: 1.81, sys: 0.03, mem: 26208 ko)
SYNTHESIZE > fiat-zig/src/p448_solinas_64.zig
fiat-zig/src/p448_solinas_64.zig (real: 2.01, user: 1.95, sys: 0.05, mem: 24804 ko)
SYNTHESIZE > fiat-zig/src/p521_64.zig
fiat-zig/src/p521_64.zig (real: 2.91, user: 2.87, sys: 0.03, mem: 24808 ko)
SYNTHESIZE > fiat-zig/src/p448_solinas_32.zig
fiat-zig/src/p448_solinas_32.zig (real: 8.21, user: 8.13, sys: 0.07, mem: 45660 ko)
OCAMLOPT src/ExtractionOCaml/word_by_word_montgomery.ml -o src/ExtractionOCaml/word_by_word_montgomery
src/ExtractionOCaml/word_by_word_montgomery (real: 55.07, user: 53.35, sys: 1.71, mem: 2103332 ko)
SYNTHESIZE > fiat-c/src/p256_64.c
fiat-c/src/p256_64.c (real: 2.02, user: 1.96, sys: 0.05, mem: 39300 ko)
SYNTHESIZE > fiat-c/src/secp256k1_64.c
fiat-c/src/secp256k1_64.c (real: 2.71, user: 2.63, sys: 0.08, mem: 43416 ko)
COQC src/ExtractionOCaml/perf_unsaturated_solinas.v > src/ExtractionOCaml/perf_unsaturated_solinas.ml
src/ExtractionOCaml/perf_unsaturated_solinas.ml (real: 19.66, user: 18.92, sys: 0.71, mem: 2080672 ko)
COQC src/ExtractionOCaml/perf_word_by_word_montgomery.v > src/ExtractionOCaml/perf_word_by_word_montgomery.ml
src/ExtractionOCaml/perf_word_by_word_montgomery.ml (real: 19.93, user: 19.20, sys: 0.73, mem: 2095128 ko)
SYNTHESIZE > fiat-json/src/p448_solinas_32.json
fiat-json/src/p448_solinas_32.json (real: 34.91, user: 34.68, sys: 0.21, mem: 56376 ko)
SYNTHESIZE > fiat-c/src/p384_64.c
fiat-c/src/p384_64.c (real: 11.40, user: 11.20, sys: 0.16, mem: 85660 ko)
SYNTHESIZE > fiat-c/src/p224_64.c
fiat-c/src/p224_64.c (real: 2.09, user: 2.04, sys: 0.05, mem: 43028 ko)
SYNTHESIZE > fiat-c/src/p256_32.c
fiat-c/src/p256_32.c (real: 28.43, user: 28.13, sys: 0.29, mem: 191204 ko)
SYNTHESIZE > fiat-rust/src/p256_64.rs
fiat-rust/src/p256_64.rs (real: 2.05, user: 2.00, sys: 0.05, mem: 40124 ko)
SYNTHESIZE > fiat-c/src/p224_32.c
fiat-c/src/p224_32.c (real: 14.26, user: 14.10, sys: 0.14, mem: 125620 ko)
SYNTHESIZE > fiat-rust/src/secp256k1_64.rs
fiat-rust/src/secp256k1_64.rs (real: 2.76, user: 2.70, sys: 0.05, mem: 46096 ko)
SYNTHESIZE > fiat-c/src/secp256k1_32.c
fiat-c/src/secp256k1_32.c (real: 32.15, user: 31.88, sys: 0.25, mem: 214188 ko)
SYNTHESIZE > fiat-c/src/p434_64.c
fiat-c/src/p434_64.c (real: 23.93, user: 23.69, sys: 0.23, mem: 135416 ko)
SYNTHESIZE > fiat-rust/src/p384_64.rs
fiat-rust/src/p384_64.rs (real: 11.03, user: 10.82, sys: 0.20, mem: 95184 ko)
SYNTHESIZE > fiat-rust/src/p224_64.rs
fiat-rust/src/p224_64.rs (real: 2.11, user: 2.03, sys: 0.07, mem: 43140 ko)
SYNTHESIZE > fiat-rust/src/p256_32.rs
fiat-rust/src/p256_32.rs (real: 31.11, user: 30.83, sys: 0.27, mem: 212496 ko)
SYNTHESIZE > fiat-rust/src/p224_32.rs
fiat-rust/src/p224_32.rs (real: 14.61, user: 14.42, sys: 0.19, mem: 114360 ko)
SYNTHESIZE > fiat-rust/src/secp256k1_32.rs
fiat-rust/src/secp256k1_32.rs (real: 32.15, user: 31.80, sys: 0.31, mem: 186884 ko)
SYNTHESIZE > fiat-rust/src/p434_64.rs
fiat-rust/src/p434_64.rs (real: 23.83, user: 23.60, sys: 0.22, mem: 153832 ko)
SYNTHESIZE > fiat-go/32/p256/p256.go
fiat-go/32/p256/p256.go (real: 31.46, user: 31.24, sys: 0.21, mem: 187340 ko)
SYNTHESIZE > fiat-go/32/secp256k1/secp256k1.go
fiat-go/32/secp256k1/secp256k1.go (real: 32.54, user: 32.15, sys: 0.34, mem: 188664 ko)
SYNTHESIZE > fiat-go/64/p256/p256.go
fiat-go/64/p256/p256.go (real: 2.00, user: 1.95, sys: 0.04, mem: 40248 ko)
SYNTHESIZE > fiat-go/64/secp256k1/secp256k1.go
fiat-go/64/secp256k1/secp256k1.go (real: 2.81, user: 2.76, sys: 0.04, mem: 40420 ko)
SYNTHESIZE > fiat-go/32/p224/p224.go
fiat-go/32/p224/p224.go (real: 14.52, user: 14.35, sys: 0.17, mem: 131916 ko)
SYNTHESIZE > fiat-go/64/p224/p224.go
fiat-go/64/p224/p224.go (real: 2.17, user: 2.11, sys: 0.05, mem: 43816 ko)
SYNTHESIZE > fiat-go/64/p384/p384.go
fiat-go/64/p384/p384.go (real: 11.11, user: 11.00, sys: 0.11, mem: 99332 ko)
SYNTHESIZE > fiat-json/src/p256_64.json
fiat-json/src/p256_64.json (real: 3.40, user: 3.33, sys: 0.07, mem: 43344 ko)
SYNTHESIZE > fiat-go/64/p434/p434.go
fiat-go/64/p434/p434.go (real: 24.03, user: 23.80, sys: 0.18, mem: 149284 ko)
SYNTHESIZE > fiat-json/src/secp256k1_64.json
fiat-json/src/secp256k1_64.json (real: 4.34, user: 4.27, sys: 0.05, mem: 42800 ko)
SYNTHESIZE > fiat-json/src/p256_32.json
fiat-json/src/p256_32.json (real: 44.34, user: 44.13, sys: 0.20, mem: 212628 ko)
SYNTHESIZE > fiat-json/src/p384_64.json
fiat-json/src/p384_64.json (real: 15.96, user: 15.79, sys: 0.17, mem: 95880 ko)
SYNTHESIZE > fiat-json/src/secp256k1_32.json
fiat-json/src/secp256k1_32.json (real: 51.20, user: 50.75, sys: 0.37, mem: 214664 ko)
SYNTHESIZE > fiat-json/src/p224_64.json
fiat-json/src/p224_64.json (real: 3.56, user: 3.48, sys: 0.07, mem: 42656 ko)
SYNTHESIZE > fiat-json/src/p224_32.json
fiat-json/src/p224_32.json (real: 22.77, user: 22.56, sys: 0.18, mem: 117224 ko)
SYNTHESIZE > fiat-json/src/p434_64.json
fiat-json/src/p434_64.json (real: 36.72, user: 36.46, sys: 0.23, mem: 151824 ko)
SYNTHESIZE > fiat-java/src/FiatP256.java
fiat-java/src/FiatP256.java (real: 28.85, user: 28.54, sys: 0.30, mem: 187028 ko)
SYNTHESIZE > fiat-java/src/FiatSecp256K1.java
fiat-java/src/FiatSecp256K1.java (real: 32.82, user: 32.37, sys: 0.44, mem: 242252 ko)
SYNTHESIZE > fiat-c/src/p384_32.c
fiat-c/src/p384_32.c (real: 495.29, user: 493.84, sys: 1.41, mem: 939020 ko)
SYNTHESIZE > fiat-java/src/FiatP224.java
fiat-java/src/FiatP224.java (real: 14.77, user: 14.53, sys: 0.23, mem: 142164 ko)
SYNTHESIZE > fiat-zig/src/p256_64.zig
fiat-zig/src/p256_64.zig (real: 2.08, user: 2.02, sys: 0.06, mem: 40512 ko)
SYNTHESIZE > fiat-rust/src/p384_32.rs
fiat-rust/src/p384_32.rs (real: 491.31, user: 490.06, sys: 1.23, mem: 1074260 ko)
SYNTHESIZE > fiat-zig/src/secp256k1_64.zig
fiat-zig/src/secp256k1_64.zig (real: 2.75, user: 2.67, sys: 0.07, mem: 39800 ko)
SYNTHESIZE > fiat-zig/src/p256_32.zig
fiat-zig/src/p256_32.zig (real: 32.11, user: 31.72, sys: 0.34, mem: 188540 ko)
SYNTHESIZE > fiat-zig/src/p384_64.zig
fiat-zig/src/p384_64.zig (real: 10.37, user: 10.17, sys: 0.19, mem: 100600 ko)
SYNTHESIZE > fiat-zig/src/secp256k1_32.zig
fiat-zig/src/secp256k1_32.zig (real: 32.63, user: 32.38, sys: 0.25, mem: 212808 ko)
SYNTHESIZE > fiat-zig/src/p224_64.zig
fiat-zig/src/p224_64.zig (real: 2.11, user: 2.05, sys: 0.06, mem: 39200 ko)
SYNTHESIZE > fiat-go/32/p384/p384.go
fiat-go/32/p384/p384.go (real: 496.31, user: 495.09, sys: 1.20, mem: 938944 ko)
SYNTHESIZE > fiat-zig/src/p224_32.zig
fiat-zig/src/p224_32.zig (real: 14.44, user: 14.23, sys: 0.21, mem: 143868 ko)
SYNTHESIZE > fiat-zig/src/p434_64.zig
fiat-zig/src/p434_64.zig (real: 23.96, user: 23.73, sys: 0.22, mem: 144088 ko)
OCAMLOPT src/ExtractionOCaml/perf_unsaturated_solinas.ml -o src/ExtractionOCaml/perf_unsaturated_solinas
src/ExtractionOCaml/perf_unsaturated_solinas (real: 29.00, user: 28.00, sys: 0.99, mem: 1054740 ko)
OCAMLOPT src/ExtractionOCaml/perf_word_by_word_montgomery.ml -o src/ExtractionOCaml/perf_word_by_word_montgomery
src/ExtractionOCaml/perf_word_by_word_montgomery (real: 33.52, user: 32.36, sys: 1.16, mem: 1053280 ko)
SYNTHESIZE > fiat-java/src/FiatP384.java
fiat-java/src/FiatP384.java (real: 424.51, user: 422.93, sys: 1.57, mem: 1074344 ko)
SYNTHESIZE > fiat-json/src/p384_32.json
fiat-json/src/p384_32.json (real: 580.05, user: 578.82, sys: 1.21, mem: 1100568 ko)
SYNTHESIZE > fiat-zig/src/p384_32.zig
fiat-zig/src/p384_32.zig (real: 441.73, user: 439.62, sys: 1.59, mem: 1028320 ko)
Makefile:111: Skipping bedrock2
make --no-print-directory -C rewriter
make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date.
echo $COQ_VERSION_INFO (8.11.1, April 2020) > .coq-version-short-date
echo $COQ_VERSION_INFO (8.11.1) > .coq-version-short
echo $COQ_VERSION_INFO (8.11.1, Apr 4 2020 17:41:20) > .coq-version-compilation-date
echo $COQ_VERSION_INFO (8.11.1, 4.06.1) > .coq-version-ocaml-version
echo $COQ_VERSION_INFO (8.11.1, <ocaml config>) > .coq-version-ocaml-config
echo $COQ_VERSION_INFO (8.11.1, <config>) > .coq-version-config
etc/machine.sh > .machine
etc/machine-extended.sh > .machine-extended
No LSB modules are available.
make[2]: Nothing to be done for 'real-all'.
make: Nothing to be done for 'perf-standalone'.
Computing file changes ...
