diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | CHANGES.md | 8 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh | 24 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected | 307 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build.log.in | 3856 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 32 |
6 files changed, 4218 insertions, 11 deletions
diff --git a/.gitignore b/.gitignore index 23e305892e..8fd9fc614c 100644 --- a/.gitignore +++ b/.gitignore @@ -64,6 +64,8 @@ time-of-build.log time-of-build-pretty.log time-of-build-before.log time-of-build-after.log +time-of-build-pretty.log2 +time-of-build-pretty.log3 .csdp.cache test-suite/.lia.cache test-suite/.nra.cache diff --git a/CHANGES.md b/CHANGES.md index bf4244bdf9..80d27d7526 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -183,6 +183,14 @@ Tools priorities, so that prefixes resolve to the most convenient bindings. The documentation pages for CoqIDE provides further details. +- The pretty timing diff scripts (flag `TIMING=1` to a + `coq_makefile`-made `Makefile`, also + `tools/make-both-single-timing-files.py`, + `tools/make-both-time-files.py`, and `tools/make-one-time-file.py`) + now correctly support non-UTF-8 characters in the output of + `coqc`/`make` as well as printing to stdout, on both python2 and + python3. + Standard Library - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh new file mode 100755 index 0000000000..e1f17725dc --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +set -x +set -e + +cd "$(dirname "${BASH_SOURCE[0]}")" + +python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log2 || exit $? +python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log3 || exit $? + +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? + +cat time-of-build.log.in | python2 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log2 || exit $? +cat time-of-build.log.in | python3 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log3 || exit $? + +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? + +(python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log2 +(python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log3 + +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected new file mode 100644 index 0000000000..05c1687002 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected @@ -0,0 +1,307 @@ +Time | File Name +----------------------------------------------------------------------- +39m02.51s | Total +----------------------------------------------------------------------- +3m26.96s | Kami/Ex/Multiplier64 +3m22.44s | bedrock2/compiler/src/FlatToRiscv +2m19.56s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI +2m11.59s | Kami/Ex/Divider64 +1m44.22s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeCSR +1m44.11s | Kami/Ex/Multiplier32 +1m41.50s | bedrock2/bedrock2/src/Examples/bsearch +1m08.57s | Kami/Ex/ProcFDInl +1m07.92s | bedrock2/deps/riscv-coq/src/Platform/MinimalMMIO +1m01.07s | Kami/Ex/FifoCorrect +1m00.73s | Kami/Ex/Divider32 +0m50.15s | bedrock2/deps/riscv-coq/src/Proofs/EncodeBound +0m40.64s | bedrock2/bedrock2/src/Examples/FE310CompilerDemo +0m40.29s | Kami/InlineFacts +0m39.12s | Kami/Renaming +0m37.44s | Kami/Ex/SimpleFifoCorrect +0m37.08s | Kami/SemFacts +0m36.08s | ─preprbedrock2/deps/coqutil/src/Map/TestGoals +0m32.76s | Kami/ModularFacts +0m28.68s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA +0m26.60s | Kami/Lib/Word +0m26.55s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_SB +0m26.45s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA64 +0m25.80s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI64 +0m25.47s | bedrock2/processor/src/KamiRiscv +0m23.66s | bedrock2/compiler/src/EmitsValid +0m22.68s | Kami/Ex/InDepthTutorial +0m22.60s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM +0m21.68s | Kami/Specialize +0m21.59s | bedrock2/bedrock2/src/Examples/lightbulb +0m19.20s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_66 +0m19.19s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_UJ +0m17.33s | Kami/Ex/ProcDecInl +0m15.63s | bedrock2/compiler/src/examples/MMIO +0m14.78s | Kami/ParametricSyntax +0m12.11s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_S +0m11.74s | bedrock2/deps/riscv-coq/src/Platform/MetricMinimal +0m09.95s | bedrock2/deps/coqutil/src/Word/Properties +0m09.77s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM64 +0m09.56s | Kami/Lib/FMap +0m09.35s | bedrock2/bedrock2/src/Examples/ipow +0m09.26s | Kami/StepDet +0m09.19s | bedrock2/bedrock2/src/WeakestPreconditionProperties +0m09.16s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_Fence +0m08.98s | Kami/RefinementFacts +0m08.68s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R_atomic +0m08.26s | bedrock2/compiler/src/FlatToRiscv32 +0m07.55s | Kami/Ex/Fifo +0m07.54s | ─ensbedrock2/deps/coqutil/src/Map/SlowGoals +0m06.99s | bedrock2/deps/riscv-coq/src/Platform/Minimal +0m06.89s | bedrock2/compiler/src/GoFlatToRiscv +0m06.82s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I +0m06.72s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_FenceI +0m06.50s | Kami/Semantics +0m06.36s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_57 +0m06.32s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R +0m06.24s | Kami/PartialInlineFacts +0m06.02s | bedrock2/deps/coqutil/src/Map/Properties +0m05.62s | Kami/Ex/ProcThreeStage +0m05.56s | Kami/Decomposition +0m05.12s | Kami/Amortization +0m05.07s | Kami/Ex/SCMMInl +0m04.71s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_system +0m04.46s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_U +0m04.19s | Kami/ParametricInline +0m04.13s | Kami/Ex/ProcDec +0m03.88s | bedrock2/bedrock2/src/Examples/swap +0m03.81s | Kami/Ex/SC +0m03.64s | bedrock2/bedrock2/src/FE310CSemantics +0m03.39s | Kami/Tutorial +0m03.30s | bedrock2/compiler/src/examples/Fibonacci +0m03.17s | Kami/Label +0m03.17s | Kami/ModuleBoundEx +0m03.10s | Kami/ParametricEquiv +0m03.06s | Kami/Wf +0m02.50s | bedrock2/compiler/src/Pipeline +0m02.42s | Kami/Ex/ProcFDInv +0m02.42s | Kami/ParamDup +0m02.39s | Kami/Duplicate +0m02.19s | Kami/ParametricWf +0m02.11s | Kami/Ex/ProcFetchDecode +0m02.06s | bedrock2/bedrock2/src/Examples/ARPResponder +0m01.94s | Kami/MapReifyEx +0m01.89s | Kami/Syntax +0m01.88s | Kami/Ex/IsaRv32/PgmGcd +0m01.87s | Kami/Ex/IsaRv32/PgmBankerWorker1 +0m01.87s | Kami/Ex/IsaRv32/PgmMatMulReport +0m01.85s | Kami/Ex/IsaRv32/PgmBankerWorker3 +0m01.83s | Kami/Ex/IsaRv32/PgmDekker2 +0m01.83s | Kami/Ex/IsaRv32/PgmFact +0m01.83s | Kami/Ex/IsaRv32/PgmMatMulNormal1 +0m01.81s | Kami/Ex/IsaRv32/PgmBankerInit +0m01.81s | Kami/Ex/IsaRv32/PgmMatMulInit +0m01.81s | Kami/Ex/IsaRv32/PgmMatMulNormal2 +0m01.81s | Kami/Ex/RegFile +0m01.80s | Kami/Ex/IsaRv32/PgmBankerWorker2 +0m01.80s | Kami/Ex/IsaRv32/PgmPeterson1 +0m01.80s | Kami/Ex/IsaRv32/PgmPeterson2 +0m01.80s | bedrock2/bedrock2/src/ptsto_bytes +0m01.78s | Kami/Ex/IsaRv32/PgmDekker1 +0m01.78s | Kami/Ex/ProcDecInv +0m01.76s | bedrock2/bedrock2/src/Map/SeparationLogic +0m01.75s | Kami/Ex/IsaRv32/PgmBsort +0m01.74s | Kami/Ex/IsaRv32/PgmHanoi +0m01.70s | Kami/Ex/NativeFifo +0m01.52s | Kami/Lib/NatLib +0m01.51s | bedrock2/processor/src/Test +0m01.48s | Kami/SymEval +0m01.47s | Kami/Ex/MemAtomic +0m01.44s | Kami/Ex/ProcThreeStInv +0m01.35s | bedrock2/bedrock2/src/Array +0m01.34s | bedrock2/bedrock2/src/TailRecursion +0m01.30s | Kami/Ex/IsaRv32 +0m01.29s | Kami/ModuleBound +0m01.29s | bedrock2/bedrock2/src/Byte +0m01.25s | bedrock2/bedrock2/src/Examples/chacha20 +0m01.19s | Kami/Ex/ProcThreeStDec +0m01.18s | bedrock2/bedrock2/src/Scalars +0m01.17s | bedrock2/deps/riscv-coq/src/Utility/ListLib +0m01.15s | Kami/Ex/OneEltFifo +0m01.14s | bedrock2/bedrock2/src/Examples/Trace +0m01.13s | bedrock2/bedrock2/src/TODO_absint +0m01.10s | bedrock2/compiler/lib/LibTactics +0m01.08s | Kami/Lib/StringAsList +0m01.00s | bedrock2/deps/coqutil/src/Z/ZLib +0m00.99s | Kami/Lib/Struct +0m00.98s | bedrock2/compiler/src/examples/toposort +0m00.95s | bedrock2/deps/riscv-coq/src/Utility/prove_Zeq_bitwise +0m00.94s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeProver +0m00.94s | bedrock2/deps/riscv-coq/src/Spec/ExecuteI +0m00.93s | Kami/Ex/ProcDecSC +0m00.92s | Kami/Ex/IsaRv32PgmExt +0m00.90s | Kami/Lib/Indexer +0m00.89s | Kami/Tactics +0m00.88s | bedrock2/compiler/src/util/ListLib +0m00.87s | Kami/Notations +0m00.84s | bedrock2/bedrock2/src/Memory +0m00.83s | Kami/Ex/ProcFDCorrect +0m00.83s | bedrock2/deps/riscv-coq/src/Utility/ZBitOps +0m00.82s | Kami/Ex/IsaRv32Pgm +0m00.82s | Kami/Lib/ilist +0m00.81s | Kami/Ex/ProcDecSCN +0m00.81s | bedrock2/deps/coqutil/src/Z/BitOps +0m00.80s | Kami/Ex/ProcFourStDec +0m00.80s | bedrock2/compiler/src/examples/EditDistExample +0m00.79s | Kami/Ext/BSyntax +0m00.79s | Kami/Ext/Extraction +0m00.77s | Kami/ParametricInlineLtac +0m00.76s | bedrock2/deps/riscv-coq/src/Platform/Example64Literal +0m00.76s | bedrock2/deps/riscv-coq/src/Spec/MetricPrimitives +0m00.75s | Kami/Ex/ProcThreeStInl +0m00.74s | Kami/Kami +0m00.74s | bedrock2/compiler/src/examples/CompileExamples +0m00.74s | bedrock2/compiler/src/examples/swap_bytes_over_uart_hexdump +0m00.74s | bedrock2/deps/riscv-coq/src/Platform/MinimalLogging +0m00.72s | Kami/Substitute +0m00.72s | bedrock2/compiler/src/examples/TestExprImp +0m00.72s | bedrock2/deps/riscv-coq/src/Spec/Primitives +0m00.71s | Kami/Ex/MemTypes +0m00.71s | bedrock2/compiler/src/examples/InlineAssemblyMacro +0m00.71s | bedrock2/compiler/src/examples/TestFlatImp +0m00.71s | bedrock2/deps/riscv-coq/src/Platform/Memory +0m00.71s | bedrock2/deps/riscv-coq/src/Spec/Decode +0m00.70s | Kami/Inline +0m00.70s | Kami/Lib/StringAsOT +0m00.69s | bedrock2/compiler/src/FlatToRiscvDef +0m00.68s | bedrock2/compiler/src/Rem4 +0m00.67s | Kami/SymEvalTac +0m00.67s | bedrock2/compiler/src/SimplWordExpr +0m00.67s | bedrock2/deps/riscv-coq/src/Utility/Encode +0m00.66s | bedrock2/bedrock2/src/Semantics +0m00.63s | Kami/Lib/StringStringAsOT +0m00.63s | bedrock2/deps/coqutil/src/Datatypes/PropSet +0m00.61s | bedrock2/compiler/src/UnmappedMemForExtSpec +0m00.61s | bedrock2/deps/riscv-coq/src/Utility/Monads +0m00.60s | bedrock2/deps/coqutil/src/Map/SortedList +0m00.59s | Kami/Synthesize +0m00.59s | bedrock2/compiler/src/util/Common +0m00.59s | bedrock2/deps/coqutil/src/Map/SortedListWord +0m00.58s | bedrock2/deps/coqutil/src/Word/Naive +0m00.58s | bedrock2/deps/riscv-coq/src/Utility/runsToNonDet_Run +0m00.57s | bedrock2/bedrock2/src/BasicC64Semantics +0m00.57s | bedrock2/deps/riscv-coq/src/Utility/Utility +0m00.56s | Kami/Lib/WordSupport +0m00.56s | bedrock2/bedrock2/src/WeakestPrecondition +0m00.55s | Kami/Lib/StringEq +0m00.55s | bedrock2/bedrock2/src/BasicC32Semantics +0m00.55s | bedrock2/compiler/src/examples/highlevel/FuncMut +0m00.55s | bedrock2/deps/riscv-coq/src/Spec/ExecuteI64 +0m00.55s | bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl32 +0m00.54s | bedrock2/bedrock2/src/Examples/MultipleReturnValues +0m00.53s | bedrock2/compiler/src/RegAlloc2 +0m00.53s | bedrock2/deps/riscv-coq/src/Spec/ExecuteM +0m00.52s | bedrock2/bedrock2/src/ProgramLogic +0m00.52s | bedrock2/deps/riscv-coq/src/Platform/Run +0m00.52s | bedrock2/deps/riscv-coq/src/Spec/ExecuteM64 +0m00.52s | bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl64 +0m00.52s | bedrock2/deps/riscv-coq/src/Utility/Words32Naive +0m00.50s | bedrock2/bedrock2/src/BasicCSyntax +0m00.50s | bedrock2/compiler/src/Basic32Semantics +0m00.50s | bedrock2/compiler/src/RegAlloc3 +0m00.49s | bedrock2/bedrock2/src/BytedumpTest +0m00.49s | bedrock2/bedrock2/src/BytedumpTestα +0m00.49s | bedrock2/deps/coqutil/src/Map/Z_keyed_SortedListMap +0m00.49s | bedrock2/deps/riscv-coq/src/Spec/Machine +0m00.49s | bedrock2/deps/riscv-coq/src/Utility/MkMachineWidth +0m00.49s | bedrock2/deps/riscv-coq/src/Utility/Words64Naive +0m00.48s | bedrock2/bedrock2/src/ToCString +0m00.48s | bedrock2/compiler/src/SeparationLogic +0m00.48s | bedrock2/deps/coqutil/src/Decidable +0m00.48s | bedrock2/deps/riscv-coq/src/Platform/MetricRiscvMachine +0m00.48s | bedrock2/deps/riscv-coq/src/Platform/RiscvMachine +0m00.47s | bedrock2/bedrock2/src/BasicC64Syntax +0m00.47s | bedrock2/deps/riscv-coq/src/Spec/PseudoInstructions +0m00.46s | bedrock2/compiler/src/ZNameGen +0m00.46s | bedrock2/deps/riscv-coq/src/Platform/MetricLogging +0m00.45s | bedrock2/compiler/src/RegAllocAnnotatedNotations +0m00.45s | bedrock2/processor/src/KamiWord +0m00.44s | bedrock2/deps/coqutil/src/Map/SortedListString_test +0m00.44s | bedrock2/deps/coqutil/src/Tactics/Tactics +0m00.44s | bedrock2/deps/riscv-coq/src/Spec/Execute +0m00.44s | bedrock2/deps/riscv-coq/src/Utility/InstructionNotations +0m00.43s | bedrock2/bedrock2/src/Map/Separation +0m00.43s | bedrock2/compiler/src/RiscvWordProperties +0m00.43s | bedrock2/deps/riscv-coq/src/Spec/VirtualMemory +0m00.43s | bedrock2/deps/riscv-coq/src/Utility/InstructionCoercions +0m00.42s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncode +0m00.40s | bedrock2/compiler/src/util/Tactics +0m00.40s | bedrock2/deps/coqutil/src/Map/Interface +0m00.39s | bedrock2/deps/coqutil/src/Z/HexNotation +0m00.38s | Kami/Lib/CommonTactics +0m00.38s | Kami/Lib/Nomega +0m00.38s | bedrock2/bedrock2/src/ZNamesSyntax +0m00.37s | bedrock2/deps/coqutil/src/Map/Funext +0m00.37s | bedrock2/deps/riscv-coq/src/Utility/div_mod_to_quot_rem +0m00.36s | Kami/Ex/Names +0m00.36s | Kami/Lib/Concat +0m00.36s | bedrock2/bedrock2/src/string2ident +0m00.36s | bedrock2/compiler/src/Simp +0m00.36s | bedrock2/deps/coqutil/src/Map/Solver +0m00.36s | bedrock2/deps/riscv-coq/src/Utility/nat_div_mod_to_quot_rem +0m00.35s | Kami/Lib/Misc +0m00.35s | bedrock2/bedrock2/src/Examples/StructAccess +0m00.35s | bedrock2/bedrock2/src/StructNotations +0m00.35s | bedrock2/deps/coqutil/src/Map/Empty_set_keyed_map +0m00.35s | bedrock2/deps/coqutil/src/Map/SortedListString +0m00.34s | Kami/Lib/Reflection +0m00.34s | bedrock2/bedrock2/src/Bytedump +0m00.34s | bedrock2/deps/riscv-coq/src/Utility/Tactics +0m00.33s | bedrock2/bedrock2/src/NotationsCustomEntry +0m00.33s | bedrock2/compiler/src/util/MyOmega +0m00.32s | bedrock2/bedrock2/src/Hexdump +0m00.32s | bedrock2/compiler/src/NameGen +0m00.31s | bedrock2/compiler/lib/LibTacticsMin +0m00.30s | bedrock2/bedrock2/src/StringNamesSyntax +0m00.30s | bedrock2/compiler/src/util/Set +0m00.30s | bedrock2/compiler/src/util/SetSolverTests +0m00.29s | bedrock2/deps/coqutil/src/Datatypes/String +0m00.27s | bedrock2/deps/coqutil/src/Word/LittleEndian +0m00.27s | bedrock2/deps/riscv-coq/src/Utility/MonadTests +0m00.26s | bedrock2/deps/coqutil/src/Z/div_mod_to_equations +0m00.23s | bedrock2/deps/riscv-coq/src/Utility/MonadT +0m00.19s | bedrock2/bedrock2/src/NotationsInConstr +0m00.19s | bedrock2/deps/coqutil/src/Datatypes/HList +0m00.17s | Kami/Lib/VectorFacts +0m00.17s | bedrock2/deps/riscv-coq/src/Utility/JMonad +0m00.14s | Kami/Lib/DepEq +0m00.13s | Kami/Lib/FinNotations +0m00.13s | bedrock2/bedrock2/src/ListPred +0m00.13s | bedrock2/bedrock2/src/Variables +0m00.13s | bedrock2/deps/coqutil/src/Datatypes/List +0m00.12s | bedrock2/deps/riscv-coq/src/Utility/MonadNotations +0m00.09s | bedrock2/bedrock2/src/Lift1Prop +0m00.09s | bedrock2/deps/coqutil/src/Datatypes/Option +0m00.09s | bedrock2/deps/coqutil/src/Datatypes/Prod +0m00.07s | Kami/Lib/BasicLogic +0m00.07s | bedrock2/bedrock2/src/Syntax +0m00.06s | Kami/Lib/DepEqNat +0m00.06s | bedrock2/deps/coqutil/src/Macros/symmetry +0m00.05s | bedrock2/compiler/lib/fiat_crypto_tactics/Not +0m00.05s | bedrock2/compiler/src/util/Misc +0m00.05s | bedrock2/deps/riscv-coq/src/Utility/PowerFunc +0m00.05s | bedrock2/deps/riscv-coq/src/Utility/runsToNonDet +0m00.04s | bedrock2/bedrock2/src/Markers +0m00.04s | bedrock2/bedrock2/src/Notations +0m00.04s | bedrock2/compiler/lib/fiat_crypto_tactics/Test +0m00.04s | bedrock2/compiler/lib/fiat_crypto_tactics/UniquePose +0m00.04s | bedrock2/compiler/src/NoActionSyntaxParams +0m00.04s | bedrock2/compiler/src/eqexact +0m00.04s | bedrock2/compiler/src/examples/highlevel/For +0m00.04s | bedrock2/compiler/src/on_hyp_containing +0m00.04s | bedrock2/compiler/src/util/Learning +0m00.04s | bedrock2/deps/coqutil/src/Datatypes/PrimitivePair +0m00.04s | bedrock2/deps/coqutil/src/Macros/subst +0m00.04s | bedrock2/deps/coqutil/src/Macros/unique +0m00.04s | bedrock2/deps/coqutil/src/Tactics/eabstract +0m00.04s | bedrock2/deps/coqutil/src/Tactics/letexists +0m00.04s | bedrock2/deps/coqutil/src/Tactics/rdelta +0m00.04s | bedrock2/deps/coqutil/src/Tactics/syntactic_unify +0m00.04s | bedrock2/deps/coqutil/src/dlet +0m00.04s | bedrock2/deps/coqutil/src/sanity +0m00.04s | bedrock2/deps/riscv-coq/src/Utility/MMIOTrace +0m00.03s | bedrock2/compiler/src/util/LogGoal
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build.log.in new file mode 100644 index 0000000000..a306586175 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build.log.in @@ -0,0 +1,3856 @@ +bedrock2/deps/coqutil/src/Tactics/eabstract (real: 0.17, user: 0.04, sys: 0.03, mem: 55016 ko) +bedrock2/deps/coqutil/src/sanity (real: 0.18, user: 0.04, sys: 0.03, mem: 54804 ko) +bedrock2/deps/coqutil/src/Tactics/letexists (real: 0.17, user: 0.04, sys: 0.03, mem: 55296 ko) +bedrock2/deps/coqutil/src/Tactics/rdelta (real: 0.17, user: 0.04, sys: 0.04, mem: 54916 ko) +bedrock2/deps/coqutil/src/Macros/subst (real: 0.16, user: 0.04, sys: 0.03, mem: 54100 ko) +bedrock2/deps/coqutil/src/dlet (real: 0.17, user: 0.04, sys: 0.03, mem: 54440 ko) +File "bedrock2/deps/coqutil/src/Datatypes/PrimitivePair.v", line 9, characters 2-67: +Warning: Notation "_ * _" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/PrimitivePair.v", line 11, characters 2-63: +Warning: Notation "{ _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/PrimitivePair.v", line 14, characters 2-67: +Warning: Notation "{ _ : _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +bedrock2/deps/coqutil/src/Macros/unique (real: 0.16, user: 0.04, sys: 0.03, mem: 54384 ko) +File "bedrock2/deps/coqutil/src/Datatypes/PrimitivePair.v", line 15, characters 2-73: +Warning: Notation "{ ' _ : _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/PrimitivePair.v", line 17, characters 2-70: +Warning: Notation "( _ , _ , .. , _ )" was already used in scope core_scope. +[notation-overridden,parsing] +bedrock2/deps/coqutil/src/Datatypes/PrimitivePair (real: 0.17, user: 0.04, sys: 0.03, mem: 56232 ko) +bedrock2/deps/coqutil/src/Datatypes/List (real: 0.58, user: 0.13, sys: 0.09, mem: 142420 ko) +bedrock2/deps/coqutil/src/Datatypes/String (real: 0.85, user: 0.29, sys: 0.16, mem: 252176 ko) +bedrock2/deps/coqutil/src/Datatypes/Option (real: 0.37, user: 0.09, sys: 0.06, mem: 108600 ko) +make[1]: Entering directory 'bedrock2' +make -C bedrock2/deps/coqutil +make[2]: Entering directory 'bedrock2/deps/coqutil' +/builds/coq/coq/_install_ci/bin/coq_makefile -f _CoqProject INSTALLDEFAULTROOT = coqutil -arg "-async-proofs-tac-j 1" bedrock2/deps/coqutil/src/Tactics/Tactics.v bedrock2/deps/coqutil/src/Tactics/eabstract.v bedrock2/deps/coqutil/src/Tactics/letexists.v bedrock2/deps/coqutil/src/Tactics/rdelta.v bedrock2/deps/coqutil/src/Tactics/syntactic_unify.v bedrock2/deps/coqutil/src/dlet.v bedrock2/deps/coqutil/src/Map/Funext.v bedrock2/deps/coqutil/src/Map/Empty_set_keyed_map.v bedrock2/deps/coqutil/src/Map/SortedListString.v bedrock2/deps/coqutil/src/Map/Z_keyed_SortedListMap.v bedrock2/deps/coqutil/src/Map/SortedListWord.v bedrock2/deps/coqutil/src/Map/Properties.v bedrock2/deps/coqutil/src/Map/TestLemmas.v bedrock2/deps/coqutil/src/Map/Interface.v bedrock2/deps/coqutil/src/Map/TestGoals.v bedrock2/deps/coqutil/src/Map/SlowGoals.v bedrock2/deps/coqutil/src/Map/SortedListString_test.v bedrock2/deps/coqutil/src/Map/Solver.v bedrock2/deps/coqutil/src/Map/SortedList.v bedrock2/deps/coqutil/src/Z/div_mod_to_equations.v bedrock2/deps/coqutil/src/Z/ZLib.v bedrock2/deps/coqutil/src/Z/HexNotation.v bedrock2/deps/coqutil/src/Z/BitOps.v bedrock2/deps/coqutil/src/Datatypes/String.v bedrock2/deps/coqutil/src/Datatypes/List.v bedrock2/deps/coqutil/src/Datatypes/PropSet.v bedrock2/deps/coqutil/src/Datatypes/Option.v bedrock2/deps/coqutil/src/Datatypes/Prod.v bedrock2/deps/coqutil/src/Datatypes/HList.v bedrock2/deps/coqutil/src/Datatypes/PrimitivePair.v bedrock2/deps/coqutil/src/Word/Naive.v bedrock2/deps/coqutil/src/Word/Properties.v bedrock2/deps/coqutil/src/Word/Interface.v bedrock2/deps/coqutil/src/Word/LittleEndian.v bedrock2/deps/coqutil/src/sanity.v bedrock2/deps/coqutil/src/Decidable.v bedrock2/deps/coqutil/src/Macros/subst.v bedrock2/deps/coqutil/src/Macros/symmetry.v bedrock2/deps/coqutil/src/Macros/unique.v -o Makefile.coq.all +make -f Makefile.coq.all +make[3]: Entering directory 'bedrock2/deps/coqutil' +COQDEP VFILES +COQC bedrock2/deps/coqutil/src/Tactics/eabstract.v +COQC bedrock2/deps/coqutil/src/sanity.v +COQC bedrock2/deps/coqutil/src/Tactics/letexists.v +COQC bedrock2/deps/coqutil/src/Tactics/rdelta.v +COQC bedrock2/deps/coqutil/src/dlet.v +COQC bedrock2/deps/coqutil/src/Macros/subst.v +COQC bedrock2/deps/coqutil/src/Macros/unique.v +COQC bedrock2/deps/coqutil/src/Datatypes/PrimitivePair.v +COQC bedrock2/deps/coqutil/src/Datatypes/List.v +COQC bedrock2/deps/coqutil/src/Datatypes/String.v +COQC bedrock2/deps/coqutil/src/Word/Interface.v +COQC bedrock2/deps/coqutil/src/Datatypes/Option.v +COQC bedbedrock2/deps/coqutil/src/Word/Interface (real: 1.40, user: 0.31, sys: 0.22, mem: 293000 ko) +bedrock2/deps/coqutil/src/Z/div_mod_to_equations (real: 0.92, user: 0.26, sys: 0.17, mem: 238732 ko) +bedrock2/deps/coqutil/src/Z/HexNotation (real: 1.24, user: 0.39, sys: 0.18, mem: 303504 ko) +bedrock2/deps/coqutil/src/Z/ZLib (real: 2.83, user: 1.00, sys: 0.28, mem: 442912 ko) +bedrock2/deps/coqutil/src/Datatypes/Prod (real: 0.32, user: 0.09, sys: 0.06, mem: 93184 ko) +bedrock2/deps/coqutil/src/Z/BitOps (real: 2.25, user: 0.81, sys: 0.26, mem: 439216 ko) +bedrock2/deps/coqutil/src/Word/Naive (real: 1.75, user: 0.58, sys: 0.27, mem: 415316 ko) +bedrock2/deps/coqutil/src/Macros/symmetry (real: 0.23, user: 0.06, sys: 0.04, mem: 67708 ko) +bedrock2/deps/coqutil/src/Decidable (real: 1.50, user: 0.48, sys: 0.23, mem: 375156 ko) +bedrock2/deps/coqutil/src/Tactics/syntactic_unify (real: 0.18, user: 0.04, sys: 0.04, mem: 56184 ko) +File "bedrock2/deps/coqutil/src/Datatypes/HList.v", line 2, characters 48-60: +Warning: Notation "_ * _" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/HList.v", line 2, characters 48-60: +Warning: Notation "{ _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/HList.v", line 2, characters 48-60: +Warning: Notation "{ _ : _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/HList.v", line 2, characters 48-60: +Warning: Notation "{ ' _ : _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/HList.v", line 2, characters 48-60: +Warning: Notation "( _ , _ , .. , _ )" was already used in scope core_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/HList.v", line 90, characters 2-19: +Warning: Notation "_ * _" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/deps/coqutil/src/Datatypes/HList.v", line 90, characters 2-19: +Warning: Notation "( _ , _ , .. , _ )" was already used in scope core_scope. +[notation-overridden,parsing] +bedrock2/deps/coqutil/src/Datatypes/HList (real: 0.63, user: 0.19, sys: 0.12, mem: 180476 ko) +bedrock2/deps/coqutil/src/Tactics/Tactics (real: 1.35, user: 0.44, sys: 0.19, mem: 321736 ko) +bedrock2/deps/coqutil/src/Word/LittleEndian (real: 0.89, user: 0.27, sys: 0.16, mem: 227732 ko) +bedrock2/deps/coqutil/src/Datatypes/PropSet (real: 1.93, user: 0.63, sys: 0.29, mem: 426168 ko) +bedrock2/deps/coqutil/src/Map/Interface (real: 1.32, user: 0.40, sys: 0.23, mem: 323944 ko) +bedrock2/deps/coqutil/src/Map/Funext (real: 1.24, user: 0.37, sys: 0.23, mem: 316400 ko) +bedrock2/deps/coqutil/src/Map/Empty_set_keyed_map (real: 1.17, user: 0.35, sys: 0.21, mem: 295952 ko) +File "bedrock2/deps/coqutil/src/Map/SortedList.v", line 110, characters 2-28: +Warning: Use of “Require” inside a section is deprecated. +[require-in-section,deprecated] +bedrock2/deps/coqutil/src/Map/SortedList (real: 1.86, user: 0.60, sys: 0.29, mem: 426440 ko) +bedrock2/deps/coqutil/src/Word/Properties (real: 21.22, user: 9.95, sys: 0.38, mem: 568468 ko) +bedrock2/deps/coqutil/src/Map/SortedListString (real: 1.20, user: 0.35, sys: 0.22, mem: 289456 ko) +bedrock2/deps/coqutil/src/Map/Z_keyed_SortedListMap (real: 1.56, user: 0.49, sys: 0.26, mem: 365272 ko) +bedrock2/deps/coqutil/src/Map/SortedListWord (real: 1.88, user: 0.59, sys: 0.30, mem: 440596 ko) +bedrock2/deps/coqutil/src/Map/Properties (real: 13.04, user: 6.02, sys: 0.32, mem: 486764 ko) +bedrock2/deps/coqutil/src/Map/SortedListString_test (real: 1.34, user: 0.44, sys: 0.21, mem: 305528 ko) +bedrock2/deps/coqutil/src/Map/Solver (real: 0.80, user: 0.36, sys: 0.21, mem: 312496 ko) +rock2/deps/coqutil/src/Z/div_mod_to_equations.v +COQC bedrock2/deps/coqutil/src/Z/ZLib.v +COQC bedrock2/deps/coqutil/src/Z/HexNotation.v +COQC bedrock2/deps/coqutil/src/Z/BitOps.v +COQC bedrock2/deps/coqutil/src/Datatypes/Prod.v +COQC bedrock2/deps/coqutil/src/Word/Naive.v +COQC bedrock2/deps/coqutil/src/Word/Properties.v +COQC bedrock2/deps/coqutil/src/Macros/symmetry.v +COQC bedrock2/deps/coqutil/src/Decidable.v +COQC bedrock2/deps/coqutil/src/Tactics/syntactic_unify.v +COQC bedrock2/deps/coqutil/src/Datatypes/HList.v +COQC bedrock2/deps/coqutil/src/Tactics/Tactics.v +COQC bedrock2/deps/coqutil/src/Word/LittleEndian.v +COQC bedrock2/deps/coqutil/src/Datatypes/PropSet.v +COQC bedrock2/deps/coqutil/src/Map/Interface.v +COQC bedrock2/deps/coqutil/src/Map/Funext.v +COQC bedrock2/deps/coqutil/src/Map/Empty_set_keyed_map.v +COQC bedrock2/deps/coqutil/src/Map/SortedList.v +COQC bedrock2/deps/coqutil/src/Map/Properties.v +COQC bedrock2/deps/coqutil/src/Map/SortedListString.v +COQC bedrock2/deps/coqutil/src/Map/Z_keyed_SortedListMap.v +COQC bedrock2/deps/coqutil/src/Map/SortedListWord.v +COQC bedrock2/deps/coqutil/src/Map/SortedListString_test.v +COQC bedrock2/deps/coqutil/src/Map/Solver.v +COQC bedrock2/deps/coqutil/src/Map/TestGoals.v +COQC bedrock2/deps/coqutil/src/Map/TestLemmas.v +Finished transaction in 0.297 secs (0.095u,0.05s) (successful) +Part 1a: Small goals (originally took <5s each) +Finished transaction in 0.35 secs (0.143u,0.032s) (successful) +Finished transaction in 0.438 secs (0.204u,0.008s) (successful) +End of TestLemmas.v +total time: 1.147s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver ---------------------------- 0.1% 99.9% 15 0.252s +─map_solver_core ----------------------- 1.0% 69.6% 15 0.209s +─map_solver_core_impl ------------------ 0.9% 68.2% 0 0.207s +─map_specialize ------------------------ 0.2% 54.9% 15 0.199s +─map_specialize_step ------------------- 24.9% 54.7% 42 0.146s +─preprocess_impl ----------------------- 1.8% 30.1% 15 0.043s +─abstract_unrecogs --------------------- 3.2% 19.8% 15 0.030s +─unrecogs_in_prop ---------------------- 15.2% 15.2% 0 0.017s +─specialize (constr_with_bindings) ----- 12.3% 12.3% 769 0.081s +─canonicalize_map_hyp ------------------ 2.3% 8.9% 316 0.011s +─unrecogs_in_option_value -------------- 3.6% 8.3% 0 0.013s +─maps_propositional -------------------- 0.3% 6.5% 15 0.009s +─ensure_no_body ------------------------ 2.1% 5.3% 602 0.006s +─assert_fails -------------------------- 1.9% 4.4% 756 0.006s +─rew_map_specs_in ---------------------- 1.3% 4.4% 316 0.010s +─canonicalize_all ---------------------- 0.6% 4.2% 15 0.006s +─maps_leaf_tac ------------------------- 0.3% 3.8% 32 0.003s +─one_rew_map_specs --------------------- 2.6% 3.5% 0 0.010s +─unrecogs_in_key ----------------------- 1.6% 2.9% 0 0.001s +─pose proof H as H' -------------------- 2.8% 2.8% 448 0.000s +─tac ----------------------------------- 1.8% 2.5% 756 0.000s +─revert_all_Props bedrock2/deps/coqutil/src/Map/TestLemmas (real: 3.68, user: 1.47, sys: 0.32, mem: 435336 ko) +---------------------- 2.1% 2.2% 15 0.003s +─autounfold (hintbases) (clause_dft_conc 2.2% 2.2% 62 0.001s +─unrecogs_in_map ----------------------- 1.4% 2.0% 0 0.002s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver ---------------------------- 0.1% 99.9% 15 0.252s + ├─map_solver_core --------------------- 1.0% 69.6% 15 0.209s + │└map_solver_core_impl ---------------- 0.9% 68.2% 0 0.207s + │ ├─map_specialize -------------------- 0.2% 54.9% 15 0.199s + │ │└map_specialize_step --------------- 24.9% 54.7% 42 0.146s + │ │ ├─specialize (constr_with_bindings) 10.7% 10.7% 448 0.081s + │ │ ├─canonicalize_map_hyp ------------ 1.2% 5.9% 154 0.011s + │ │ │└rew_map_specs_in ---------------- 0.8% 3.3% 154 0.010s + │ │ │└one_rew_map_specs --------------- 1.9% 2.5% 0 0.010s + │ │ ├─ensure_no_body ------------------ 2.1% 5.3% 602 0.006s + │ │ │└assert_fails -------------------- 1.6% 3.1% 602 0.006s + │ │ └─pose proof H as H' -------------- 2.8% 2.8% 448 0.000s + │ ├─maps_propositional ---------------- 0.3% 6.5% 15 0.009s + │ │└maps_leaf_tac --------------------- 0.3% 3.8% 32 0.003s + │ └─canonicalize_all ------------------ 0.6% 4.2% 15 0.006s + │ └canonicalize_map_hyp -------------- 1.1% 3.0% 162 0.001s + └─preprocess_impl --------------------- 1.8% 30.1% 15 0.043s + ├─abstract_unrecogs ----------------- 3.2% 19.8% 15 0.030s + │└unrecogs_in_prop ------------------ 15.2% 15.2% 0 0.017s + │└unrecogs_in_option_value ---------- 3.6% 8.3% 0 0.013s + │ ├─unrecogs_in_key ----------------- 1.1% 2.0% 0 0.001s + │ └─unrecogs_in_map ----------------- 1.4% 2.0% 0 0.002s + └─revert_all_Props ------------------ 2.1% 2.2% 15 0.003s + +COQC bedrock2/deps/coqutil/src/Map/SlowGoals.v +Finished transaction in 3.949 secs (1.835u,0.093s) (successful) +Finished transaction in 6.898 secs (3.179u,0.177s) (successful) +Finished transaction in 6.138 secs (2.811u,0.154s) (successful) +Finished transaction in 15.112 secs (7.09u,0.222s) (successful) +Finished transaction in 0.047 secs (0.024u,0.s) (successful) +End of SlowGoals.v +total time: 7.313s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver_core ----------------------- 0.0% 100.0% 1 7.312s +─map_solver_core_impl ------------------ 0.0% 100.0% 0 7.310s +─maps_propositional -------------------- 0.6% 61.3% 33 4.485s +─map_specialize ------------------------ 0.0% 38.0% 1 2.779s +─map_specialize_step ------------------- 15.8% 38.0% 37 1.817s +─maps_leaf_tac ------------------------- 0.7% 32.8% 228 0.018s +─propositional_cheap_step -------------- 25.2% 25.6% 427 0.013s +─congruence ---------------------------- 16.9% 16.9% 228 0.010s +─maps_choice_step ---------------------- 0.1% 15.7% 0 0.040s +─next ---------------------------------- 15.7% 15.7% 32 0.040s +─auto (int_or_var_opt) (auto_using) (hin 14.8% 14.8% 358 0.008s +─unify (constr) (constr) --------------- 5.5% 5.5% 4416 0.006s +─canonicalize_map_hyp ------------------ 1.0% 4.4% 822 0.008s +─specialize (constr_with_bindings) ----- 4.2% 4.2% 3293 0.008s +─ensbedrock2/deps/coqutil/src/Map/SlowGoals (real: 16.46, user: 7.54, sys: 0.41, mem: 454624 ko) +ure_no_body ------------------------ 1.5% 3.6% 3220 0.008s +─assert_fails -------------------------- 0.9% 3.2% 4005 0.008s +─pose proof H as H' -------------------- 3.0% 3.0% 2405 0.009s +─tac ----------------------------------- 1.4% 2.3% 4005 0.008s +─maps_split_step ----------------------- 0.3% 2.2% 260 0.006s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver_core ----------------------- 0.0% 100.0% 1 7.312s +└map_solver_core_impl ------------------ 0.0% 100.0% 0 7.310s + ├─maps_propositional ------------------ 0.6% 61.3% 33 4.485s + │ ├─maps_leaf_tac --------------------- 0.7% 32.8% 228 0.018s + │ │ ├─congruence ---------------------- 16.9% 16.9% 228 0.010s + │ │ └─auto (int_or_var_opt) (auto_using 14.8% 14.8% 358 0.008s + │ ├─propositional_cheap_step ---------- 25.0% 25.4% 424 0.013s + │ ├─maps_choice_step ------------------ 0.1% 15.7% 0 0.040s + │ │└next ------------------------------ 15.7% 15.7% 32 0.040s + │ └─maps_split_step ------------------- 0.3% 2.2% 260 0.006s + └─map_specialize ---------------------- 0.0% 38.0% 1 2.779s + └map_specialize_step ----------------- 15.8% 38.0% 37 1.817s + ├─unify (constr) (constr) ----------- 5.5% 5.5% 4413 0.006s + ├─canonicalize_map_hyp -------------- 0.9% 4.2% 785 0.008s + ├─ensure_no_body -------------------- 1.5% 3.6% 3220 0.008s + │└assert_fails ---------------------- 0.7% 2.1% 3220 0.008s + ├─pose proof H as H' ---------------- 3.0% 3.0% 2405 0.009s + └─specialize (constr_with_bindings) - 2.5% 2.5% 2405 0.007s + +Finished transaction in 2.274 secs (1.721u,0.068s) (successful) +Finished transaction in 1.891 secs (1.771u,0.084s) (successful) +Finished transaction in 1.713 secs (1.599u,0.076s) (successful) +Finished transaction in 0.196 secs (0.185u,0.008s) (successful) +Part 1b: Medium goals (originally took >5s each) +Finished transaction in 1.398 secs (1.318u,0.055s) (successful) +Finished transaction in 3.691 secs (3.403u,0.173s) (successful) +Finished transaction in 3.279 secs (3.017u,0.167s) (successful) +Finished transaction in 1.982 secs (1.851u,0.083s) (successful) +Finished transaction in 1.932 secs (1.8u,0.097s) (successful) +Finished transaction in 3.391 secs (3.136u,0.144s) (successful) +Finished transaction in 3.23 secs (3.024u,0.138s) (successful) +Part 1c: Large goals (originally took >50s each) +Finished transaction in 4.687 secs (4.34u,0.215s) (successful) +End of TestGoals.v +total time: 37.262s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver ---------------------------- 0.0% 100.0% 18 4.555s +─map_solver_core ----------------------- 0.0% 96.9% 18 4.483s +─map_solver_core_impl ------------------ 0.0% 96.8% 0 4.482s +─map_specialize ------------------------ 0.0% 93.4% 18 4.351s +─map_specialize_step ------------------- 43.0% 93.3% 428 1.253s +─ensure_no_body ------------------------ 5.8% 13.2% 62635 0.014s +─specialize (constr_with_bindings) ----- 12.8% 12.8% 63060 0.013s +─pose proof H as H' -------------------- 11.4% 11.4% 55172 0.009s +─assert_fails -------------------------- 3.3% 9.5% 69963 0.014s +─canonicalize_map_hyp ------------------ 1.8% 7.6% 7811 0.014s +─tac ----------------------------------- 4.2% 6.2% 69963 0.014s +─preprbedrock2/deps/coqutil/src/Map/TestGoals (real: 49.22, user: 36.08, sys: 2.04, mem: 562540 ko) +ocess_impl ----------------------- 0.1% 3.1% 18 0.116s +─Tactics.ensure_new -------------------- 1.1% 3.1% 7328 0.014s +─rew_map_specs_in ---------------------- 1.0% 3.0% 7812 0.014s +─maps_propositional -------------------- 0.0% 2.8% 22 0.231s +─abstract_unrecogs --------------------- 0.4% 2.4% 18 0.107s +─unify (constr) (constr) --------------- 2.2% 2.2% 75932 0.009s +─one_rew_map_specs --------------------- 1.4% 2.1% 0 0.014s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver ---------------------------- 0.0% 100.0% 18 4.555s + ├─map_solver_core --------------------- 0.0% 96.9% 18 4.483s + │└map_solver_core_impl ---------------- 0.0% 96.8% 0 4.482s + │ ├─map_specialize -------------------- 0.0% 93.4% 18 4.351s + │ │└map_specialize_step --------------- 43.0% 93.3% 428 1.253s + │ │ ├─ensure_no_body ------------------ 5.8% 13.2% 62635 0.014s + │ │ │└assert_fails -------------------- 2.9% 7.5% 62635 0.014s + │ │ │└tac ----------------------------- 3.3% 4.6% 62635 0.011s + │ │ ├─pose proof H as H' -------------- 11.4% 11.4% 55172 0.009s + │ │ ├─specialize (constr_with_bindings) 10.5% 10.5% 55172 0.010s + │ │ ├─canonicalize_map_hyp ------------ 1.7% 7.3% 7328 0.014s + │ │ │ ├─rew_map_specs_in -------------- 0.9% 2.9% 7328 0.014s + │ │ │ └─specialize (constr_with_binding 2.2% 2.2% 7328 0.013s + │ │ ├─Tactics.ensure_new -------------- 1.1% 3.1% 7328 0.014s + │ │ │└assert_fails -------------------- 0.4% 2.0% 7328 0.014s + │ │ └─unify (constr) (constr) --------- 2.2% 2.2% 75866 0.009s + │ └─maps_propositional ---------------- 0.0% 2.8% 22 0.231s + └─preprocess_impl --------------------- 0.1% 3.1% 18 0.116s + └abstract_unrecogs ------------------- 0.4% 2.4% 18 0.107s + +make[3]: Leaving directory 'bedrock2/deps/coqutil' +make[2]: Leaving directory 'bedrock2/deps/coqutil' +make -C bedrock2/deps/riscv-coq all +make -C bedrock2/bedrock2 +make[2]: Entering directory 'bedrock2/deps/riscv-coq' +/builds/coq/coq/_install_ci/bin/coq_makefile -f _CoqProject INSTALLDEFAULTROOT = riscv -arg "-async-proofs-tac-j 1" bedrock2/deps/riscv-coq/src/Spec/Primitives.v bedrock2/deps/riscv-coq/src/Spec/ExecuteI.v bedrock2/deps/riscv-coq/src/Spec/ExecuteI64.v bedrock2/deps/riscv-coq/src/Spec/MetricPrimitives.v bedrock2/deps/riscv-coq/src/Spec/Machine.v bedrock2/deps/riscv-coq/src/Spec/ExecuteM.v bedrock2/deps/riscv-coq/src/Spec/ExecuteM64.v bedrock2/deps/riscv-coq/src/Spec/PseudoInstructions.v bedrock2/deps/riscv-coq/src/Spec/Execute.v bedrock2/deps/riscv-coq/src/Spec/Decode.v bedrock2/deps/riscv-coq/src/Spec/VirtualMemory.v bedrock2/deps/riscv-coq/src/Utility/MMIOTrace.v bedrock2/deps/riscv-coq/src/Utility/InstructionNotations.v bedrock2/deps/riscv-coq/src/Utility/nat_div_mod_to_quot_rem.v bedrock2/deps/riscv-coq/src/Utility/prove_Zeq_bitwise.v bedrock2/deps/riscv-coq/src/Utility/InstructionCoercions.v bedrock2/deps/riscv-coq/src/Utility/Words32Naive.v bedrock2/deps/riscv-coq/src/Utility/JMonad.v bedrock2/deps/riscv-coq/src/Utility/Utility.v bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl64.v bedrock2/deps/riscv-coq/src/Utility/runsToNonDet_Run.v bedrock2/deps/riscv-coq/src/Utility/ZBitOps.v bedrock2/deps/riscv-coq/src/Utility/MonadNotations.v bedrock2/deps/riscv-coq/src/Utility/Tactics.v bedrock2/deps/riscv-coq/src/Utility/MonadTests.v bedrock2/deps/riscv-coq/src/Utility/Words64Naive.v bedrock2/deps/riscv-coq/src/Utility/Encode.v bedrock2/deps/riscv-coq/src/Utility/MkMachineWidth.v bedrock2/deps/riscv-coq/src/Utility/MonadT.v bedrock2/deps/riscv-coq/src/Utility/div_mod_to_quot_rem.v bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl32.v bedrock2/deps/riscv-coq/src/Utility/PowerFunc.v bedrock2/deps/riscv-coq/src/Utility/ListLib.v bedrock2/deps/riscv-coq/src/Utility/runsToNonDet.v bedrock2/deps/riscv-coq/src/Utility/Monads.v bedrock2/deps/riscv-coq/src/Platform/MetricLogging.v bedrock2/deps/riscv-coq/src/Platform/Example64Literal.v bedrock2/deps/riscv-coq/src/Platform/RiscvMachine.v bedrock2/deps/riscv-coq/src/Platform/MetricMinimal.v bedrock2/deps/riscv-coq/src/Platform/Example.v bedrock2/deps/riscv-coq/src/Platform/Memory.v bedrock2/deps/riscv-coq/src/Platform/MinimalLogging.v bedrock2/deps/riscv-coq/src/Platform/Run.v bedrock2/deps/riscv-coq/src/Platform/MetricRiscvMachine.v bedrock2/deps/riscv-coq/src/Platform/Minimal.v bedrock2/deps/riscv-coq/src/Platform/MinimalMMIO.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_Fence.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA64.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeCSR.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_SB.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI64.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_U.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeProver.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_FenceI.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R_atomic.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM64.v bedrock2/deps/riscv-coq/src/Proofs/EncodeBound.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_S.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncode.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_system.v bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_UJ.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_57.v bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_66.v -o Makefile.coq.all +make[2]: Entering directory 'bedrock2/bedrock2' +printf -- '-Q src bedrock2\n-Q /builds/coq/coWarning: ../coqutil/src (used in -R or -Q) is not a subdirectory of the current directory + +bedrock2/bedrock2/src/Syntax (real: 0.28, user: 0.07, sys: 0.04, mem: 93508 ko) +bedrock2/deps/riscv-coq/src/Utility/Monads (real: 1.74, user: 0.61, sys: 0.22, mem: 357880 ko) +bedrock2/deps/riscv-coq/src/Utility/Tactics (real: 1.14, user: 0.34, sys: 0.21, mem: 294376 ko) +bedrock2/bedrock2/src/Byte (real: 3.14, user: 1.29, sys: 0.27, mem: 418180 ko) +bedrock2/bedrock2/src/Notations (real: 0.16, user: 0.04, sys: 0.03, mem: 56396 ko) +bedrock2/deps/riscv-coq/src/Platform/MetricLogging (real: 1.44, user: 0.46, sys: 0.23, mem: 344552 ko) +bedrock2/deps/riscv-coq/src/Utility/MMIOTrace (real: 0.17, user: 0.04, sys: 0.03, mem: 56096 ko) +q/_build_ci/bedrock2/deps/coqutil/src coqutil\n' > _CoqProject +/builds/coq/coq/_install_ci/bin/coq_makefile -f _CoqProject INSTALLDEFAULTROOT = bedrock2 -arg "-async-proofs-tac-j 1" bedrock2/bedrock2/src/BasicCSyntax.v bedrock2/bedrock2/src/ToCString.v bedrock2/bedrock2/src/BytedumpTest.v bedrock2/bedrock2/src/BasicC32Semantics.v bedrock2/bedrock2/src/Byte.v bedrock2/bedrock2/src/Variables.v bedrock2/bedrock2/src/Semantics.v bedrock2/bedrock2/src/div10.v bedrock2/bedrock2/src/NotationsCustomEntry.v bedrock2/bedrock2/src/ListPred.v bedrock2/bedrock2/src/BasicC64Semantics.v bedrock2/bedrock2/src/Map/SeparationLogic.v bedrock2/bedrock2/src/Map/Separation.v bedrock2/bedrock2/src/Syntax.v bedrock2/bedrock2/src/WeakestPreconditionProperties.v bedrock2/bedrock2/src/NotationsInConstr.v bedrock2/bedrock2/src/WeakestPrecondition.v bedrock2/bedrock2/src/TODO_absint.v bedrock2/bedrock2/src/Bytedump.v bedrock2/bedrock2/src/FE310CSemantics.v bedrock2/bedrock2/src/StructNotations.v bedrock2/bedrock2/src/Examples/lightbulb.v bedrock2/bedrock2/src/Examples/MultipleReturnValues.v bedrock2/bedrock2/src/Examples/ARPResponder.v bedrock2/bedrock2/src/Examples/swap.v bedrock2/bedrock2/src/Examples/chacha20.v bedrock2/bedrock2/src/Examples/Demos.v bedrock2/bedrock2/src/Examples/bsearch.v bedrock2/bedrock2/src/Examples/Trace.v bedrock2/bedrock2/src/Examples/StructAccess.v bedrock2/bedrock2/src/Examples/FE310CompilerDemo.v bedrock2/bedrock2/src/Examples/ipow.v bedrock2/bedrock2/src/Markers.v bedrock2/bedrock2/src/Memory.v bedrock2/bedrock2/src/Structs.v bedrock2/bedrock2/src/Notations.v bedrock2/bedrock2/src/ProgramLogic.v bedrock2/bedrock2/src/Hexdump.v bedrock2/bedrock2/src/BasicC64Syntax.v bedrock2/bedrock2/src/Scalars.v bedrock2/bedrock2/src/string2ident.v bedrock2/bedrock2/src/ptsto_bytes.v bedrock2/bedrock2/src/StringNamesSyntax.v bedrock2/bedrock2/src/Lift1Prop.v bedrock2/bedrock2/src/ZNamesSyntax.v bedrock2/bedrock2/src/TailRecursion.v bedrock2/bedrock2/src/Array.v -o Makefile.coq.all +make -f Makefile.coq.all +make -f Makefile.coq.all +make[3]: Entering directory 'bedrock2/deps/riscv-coq' +make[3]: Entering directory 'bedrock2/bedrock2' +COQDEP VFILES +COQDEP VFILES +COQC bedrock2/bedrock2/src/Syntax.v +COQC bedrock2/deps/riscv-coq/src/Utility/Monads.v +COQC bedrock2/bedrock2/src/Byte.v +COQC bedrock2/deps/riscv-coq/src/Utility/Tactics.v +COQC bedrock2/deps/riscv-coq/src/Platform/MetricLogging.v +COQC bedrock2/bedrock2/src/Notations.v +COQC bedrock2/bedrock2/src/div10.v +COQC bedrock2/deps/riscv-coq/src/Utility/MMIOTrace.v +COQC bedrock2/deps/riscv-coq/src/Utility/nat_div_mbedrock2/bedrock2/src/div10 (real: 1.82, user: 0.61, sys: 0.29, mem: 437628 ko) +bedrock2/deps/riscv-coq/src/Utility/nat_div_mod_to_quot_rem (real: 1.14, user: 0.36, sys: 0.19, mem: 298516 ko) +File "bedrock2/bedrock2/src/NotationsCustomEntry.v", line 50, characters 0-51: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bedrock_nontail.". [undeclared-scope,deprecated] +File "bedrock2/bedrock2/src/NotationsCustomEntry.v", line 142, characters 0-45: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bedrock_tail.". [undeclared-scope,deprecated] +File "bedrock2/deps/riscv-coq/src/Utility/JMonad.v", line 13, characters 0-102: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] +bedrock2/bedrock2/src/NotationsCustomEntry (real: 1.07, user: 0.33, sys: 0.18, mem: 301112 ko) +bedrock2/deps/riscv-coq/src/Utility/JMonad (real: 0.64, user: 0.17, sys: 0.13, mem: 184664 ko) +bedrock2/bedrock2/src/ListPred (real: 0.47, user: 0.13, sys: 0.09, mem: 144616 ko) +File "bedrock2/deps/riscv-coq/src/Utility/MonadNotations.v", line 3, characters 0-102: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] +bedrock2/deps/riscv-coq/src/Utility/MonadNotations (real: 0.48, user: 0.12, sys: 0.11, mem: 146976 ko) +bedrock2/deps/riscv-coq/src/Utility/PowerFunc (real: 0.20, user: 0.05, sys: 0.04, mem: 65768 ko) +bedrock2/bedrock2/src/Lift1Prop (real: 0.32, user: 0.09, sys: 0.06, mem: 116312 ko) +File "bedrock2/deps/riscv-coq/src/Utility/MonadTests.v", line 10, characters 0-102: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] +File "bedrock2/bedrock2/src/NotationsInConstr.v", line 5, characters 0-43: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bedrock_var.". [undeclared-scope,deprecated] +File "bedrock2/bedrock2/src/NotationsInConstr.v", line 7, characters 0-45: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bedrock_expr.". [undeclared-scope,deprecated] +File "bedrock2/bedrock2/src/NotationsInConstr.v", line 21, characters 0-43: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bedrock_cmd.". [undeclared-scope,deprecated] +File "bedrock2/bedrock2/src/NotationsInConstr.v", line 46, characters 0-55: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bedrock_func_body.". [undeclared-scope,deprecated] +bedrock2/bedrock2/src/NotationsInConstr (real: 0.66, user: 0.19, sys: 0.10, mem: 172428 ko) +bedrock2/deps/riscv-coq/src/Utility/MonadTests (real: 0.93, user: 0.27, sys: 0.16, mem: 255852 ko) +File "bedrock2/deps/riscv-coq/src/Utility/MonadT.v", line 17, characters 0-102: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] +File "bedrock2/deps/riscv-coq/src/Utility/MonadT.v", line 265, characters 2-23: +Warning: State is declared as a local axiom [local-declaration,scope] +File "bedrock2/deps/riscv-coq/src/Utility/MonadT.v", line 266, characters 2-37: +Warning: step is declared as a local axiom [local-declaration,scope] +File "bedrock2/deps/riscv-coq/src/Utility/MonadT.v", line 280, characters 2-23: +Warning: State is declared as a local axiom [local-declaration,scope] +File "bedrock2/deps/riscv-coq/src/Utility/MonadT.v", line 281, characters 2-37: +Warning: step is declared as a local axiom [local-declaration,scope] +File "bedrock2/deps/riscv-coq/src/Utility/MonadT.v", line 311, characters 2-27: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +bedrock2/deps/riscv-coq/src/Utility/MonadT (real: 0.78, user: 0.23, sys: 0.15, mem: 212520 ko) +od_to_quot_rem.v +COQC bedrock2/bedrock2/src/NotationsCustomEntry.v +COQC bedrock2/deps/riscv-coq/src/Utility/JMonad.v +COQC bedrock2/bedrock2/src/ListPred.v +COQC bedrock2/deps/riscv-coq/src/Utility/MonadNotations.v +COQC bedrock2/bedrock2/src/Lift1Prop.v +COQC bedrock2/deps/riscv-coq/src/Utility/PowerFunc.v +COQC bedrock2/deps/riscv-coq/src/Utility/MonadTests.v +COQC bedrock2/bedrock2/src/NotationsInConstr.v + = [(3, true); (3, false); (4, true); (4, false)] + : Id (list (nat * bool)) + = None + : Id (option (list nat)) + = [Some 3; Some 4; None] + : Id (list (option nat)) + = (tt, 5) + : Id (unit * nat) + = [(tt, 6); (tt, 7)] + : Id (list (unit * nat)) + = [0; 1; 2; 3] + : list nat + = [(tt, 0); (tt, 1); (tt, 2); (tt, 3)] + : Id (list (unit * nat)) +COQC bedrock2/bedrock2/src/Structs.v + = ([(0, 1); (0, 0)], (0, 0)) + : Id (list (nat * nat) * (nat * nat)) + = [(0, 1, (0, 1)); (1, 0, (1, 0))] + : Id (list (nat * nat * (nat * nat))) + = ([0; 1; 2; 3], 3) + : Id (list nat * nat) + = ([0; 5; 6; 15], 15) + : Id (list nat * nat) + = (tt, <<20,10,10>>) + : Id (unit * Regs) + = ([<<0,20,30>>; <<1,20,30>>; <<2,20,30>>], <<2,20,30>>) + : Id (list Regs * Regs) + = ([<<0,11,11>>; <<1,11,11>>; <<2,11,11>>; <<3,11,11>>], <<3,11,11>>) + : Id (list Regs * Regs) +COQC bedrock2/deps/riscv-coq/src/Utility/MonadT.v + = list (option nat) + : Type + = fun (A : Type) (aset : (A -> Prop) -> Prop) + (f : (A -> Prop) -> A) (b : A) => + exists a : A -> Prop, aset a /\ f a = b + : forall A : Type, + ((A -> Prop) -> Prop) -> ((A -> Prop) -> A) -> A -> Prop +runsTo_ind + : forall (initial : State) (P : State -> Prop) (P0 : Prop), + (P initial -> P0) -> + ((forall omid : option State, + step initial omid -> + exists mid : State, omid = Some mid /\ runsTo mid P) -> P0) -> + runsTo initial P -> P0 +runsTo_ind = +fun (initial : State) (P : State -> Prop) (P0 : Prop) + (f : P initial -> P0) + (f0 : (forall omid : option (option unit * State), + step initial omid -> + exists mid : State, omid = Some (Some tt, mid) /\ runsTo mid P) -> + P0) (r : runsTo initial P) => +match r with +| runsToDone _ _ x => f x +| runsToStep _ _ x => f0 x +end + : forall (initial : State) (P : State -> Prop) (P0 : Prop), + (P initial -> P0) -> + ((forall omid : option (option unit * State), + step initial omid -> + exists mid : State, omid = Some (Some tt, mid) /\ runsTo mid P) -> + P0) -> runsTo initial P -> P0 + +Argument scopes are [_ function_scope type_scope function_scope + function_scope _] +Closed under the global context +COQC bedrock2/deps/riscv-coq/src/Utility/ListLib.v + = 4%Z + : Z + = 20%Z + : Z + = 30%Z + : Z + = 90%Z + : Z + = inr + (Struct + (("first", Array 15 (Bytes 1)) + :: ("last", Array 15 (Bytes 1)) :: nil), 30%Z) + : PathError Z + type * Z + = inr (Array 15 (Bytes 1), 45%Z) + : PathError Z + type * Z + = inr (Bytes 1, 47%Z) + : PathError Z + type * Z + = fun (p : parameters) (add mul : bopname) (base : expr) => + inr + (Struct + (("first", Array 15 (Bytes 1)) + :: ("last", Array 15 (Bytes 1)) :: nil), + expr.op add base (expr.op mul (expr.literal 1) (expr.literal 30))) + : forall p : parameters, + bopname -> bopname -> expr -> PathError expr + type * expr + = fun (p : parameters) (add mul : bopname) (base : expr) => + inr + (Array 15 (Bytes 1), + expr.op add + (expr.op add base (expr.op mul (expr.literal 1) (expr.literal 30))) + (expr.literal 15)) + : forall p : parameters, + bopname -> bopname -> expr -> PathError expr + type * bedrock2/bedrock2/src/Structs (real: 1.31, user: 0.44, sys: 0.20, mem: 308516 ko) +File "bedrock2/bedrock2/src/Markers.v", line 19, characters 2-71: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope hide_markers.". [undeclared-scope,deprecated] +bedrock2/bedrock2/src/Markers (real: 0.18, user: 0.04, sys: 0.04, mem: 57444 ko) +bedrock2/bedrock2/src/string2ident (real: 1.15, user: 0.36, sys: 0.20, mem: 272052 ko) +File "bedrock2/bedrock2/src/Hexdump.v", line 16, characters 0-41: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope hexdump_scope.". [undeclared-scope,deprecated] +bedrock2/bedrock2/src/Hexdump (real: 1.06, user: 0.32, sys: 0.19, mem: 274924 ko) +bedrock2/deps/riscv-coq/src/Utility/ListLib (real: 2.96, user: 1.17, sys: 0.28, mem: 444076 ko) +bedrock2/bedrock2/src/ZNamesSyntax (real: 1.16, user: 0.38, sys: 0.18, mem: 294268 ko) +bedrock2/deps/riscv-coq/src/Utility/div_mod_to_quot_rem (real: 1.14, user: 0.37, sys: 0.18, mem: 295668 ko) +File "bedrock2/deps/riscv-coq/src/Utility/runsToNonDet.v", line 20, characters 2-27: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "bedrock2/deps/riscv-coq/src/Utility/runsToNonDet.v", line 30, characters 2-28: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +bedrock2/deps/riscv-coq/src/Utility/runsToNonDet (real: 0.20, user: 0.05, sys: 0.03, mem: 65120 ko) +bedrock2/bedrock2/src/Variables (real: 0.46, user: 0.13, sys: 0.09, mem: 149744 ko) +bedrock2/bedrock2/src/StringNamesSyntax (real: 1.02, user: 0.30, sys: 0.18, mem: 252388 ko) +File "bedrock2/bedrock2/src/Bytedump.v", line 2, characters 0-43: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bytedump_scope.". [undeclared-scope,deprecated] +bedrock2/bedrock2/src/Bytedump (real: 1.08, user: 0.34, sys: 0.18, mem: 272812 ko) +bedrock2/deps/riscv-coq/src/Utility/ZBitOps (real: 2.28, user: 0.83, sys: 0.28, mem: 439724 ko) +File "bedrock2/deps/riscv-coq/src/Utility/Utility.v", line 120, characters 0-78: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope alu_scope.". [undeclared-scope,deprecated] +bedrock2/deps/riscv-coq/src/Utility/Utility (real: 1.69, user: 0.57, sys: 0.25, mem: 358716 ko) +bedrock2/bedrock2/src/Memory (real: 2.40, user: 0.84, sys: 0.30, mem: 443020 ko) +bedrock2/bedrock2/src/Map/Separation (real: 1.31, user: 0.43, sys: 0.20, mem: 289244 ko) +bedrock2/deps/riscv-coq/src/Utility/prove_Zeq_bitwise (real: 2.66, user: 0.95, sys: 0.32, mem: 441452 ko) +bedrock2/bedrock2/src/StructNotations (real: 1.10, user: 0.35, sys: 0.18, mem: 267768 ko) +bedrock2/deps/riscv-coq/src/Utility/Words32Naive (real: 1.51, user: 0.52, sys: 0.21, mem: 346660 ko) +bedrock2/bedrock2/src/ToCString (real: 1.34, user: 0.48, sys: 0.17, mem: 276676 ko) +bedrock2/deps/riscv-coq/src/Utility/Words64Naive (real: 1.41, user: 0.49, sys: 0.19, mem: 346980 ko) +bedrock2/bedrock2/src/BytedumpTest (real: 1.52, user: 0.49, sys: 0.25, mem: 411496 ko) +bedrock2/bedrock2/src/BytedumpTestα (real: 1.52, user: 0.49, sys: 0.25, mem: 411496 ko) +bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl32 (real: 1.64, user: 0.55, sys: 0.23, mem: 376020 ko) +bedrock2/bedrock2/src/Semantics (real: 1.81, user: 0.66, sys: 0.26, mem: 441912 ko) +bedrock2/deps/riscv-coq/src/Spec/Decode (real: 2.09, user: 0.71, sys: 0.28, mem: 446048 ko) +bedrock2/deps/riscv-coq/src/Platform/Memory (real: 2.06, user: 0.71, sys: 0.27, mem: 449484 ko) +bedrock2/bedrock2/src/Map/SeparationLogic (real: 4.20, user: 1.76, sys: 0.27, mem: 433996 ko) +bedrock2/deps/riscv-coq/src/Spec/Machine (real: 1.50, user: 0.49, sys: 0.24, mem: 375808 ko) +bedrock2/bedrock2/src/WeakestPrecondition (real: 1.67, user: 0.56, sys: 0.24, mem: 410516 ko) +bedrock2/deps/riscv-coq/src/Platform/RiscvMachine (real: 1.48, user: 0.48, sys: 0.24, mem: 370692 ko) +bedrock2/deps/riscv-coq/src/Utility/MkMachineWidth (real: 1.44, user: 0.49, sys: 0.21, mem: 360632 ko) +bedrock2/bedrock2/src/Array (real: 3.30, user: 1.35, sys: 0.27, mem: 457132 ko) +bedrock2/deps/riscv-coq/src/Spec/VirtualMemory (real: 1.33, user: 0.43, sys: 0.22, mem: 321032 ko) +bedrock2/bedrock2/src/BasicC64Syntax (real: 1.40, user: 0.47, sys: 0.21, mem: 321560 ko) +bedrock2/deps/riscv-coq/src/Platform/MetricRiscvMachine (real: 1.49, user: 0.48, sys: 0.24, mem: 362608 ko) +bedrock2/deps/riscv-coq/src/Spec/ExecuteM (real: 1.62, user: 0.53, sys: 0.26, mem: 387416 ko) +bedrock2/bedrock2/src/Examples/Trace (real: 2.96, user: 1.14, sys: 0.29, mem: 449412 ko) +bedrock2/deps/riscv-coq/src/Spec/ExecuteM64 (real: 1.64, user: 0.52, sys: 0.25, mem: 375816 ko) +bedrock2/bedrock2/src/Examples/StructAccess (real: 1.12, user: 0.35, sys: 0.19, mem: 272888 ko) +bedrock2/deps/riscv-coq/src/Spec/PseudoInstructions (real: 1.40, user: 0.47, sys: 0.21, mem: 338992 ko) +bedrock2/bedrock2/src/BasicCSyntax (real: 1.40, user: 0.50, sys: 0.18, mem: 322924 ko) +expr + = fun (p : parameters) (add mul : bopname) (base : expr) => + inr + (Bytes 1, + expr.op add + (expr.op add + (expr.op add base + (expr.op mul (expr.literal 1) (expr.literal 30))) + (expr.literal 15)) + (expr.op mul (expr.literal 2) (expr.literal 1))) + : forall p : parameters, + bopname -> bopname -> expr -> PathError expr + type * expr +COQC bedrock2/bedrock2/src/Markers.v +COQC bedrock2/bedrock2/src/string2ident.v +COQC bedrock2/bedrock2/src/Hexdump.v +COQC bedrock2/bedrock2/src/ZNamesSyntax.v +COQC bedrock2/deps/riscv-coq/src/Utility/div_mod_to_quot_rem.v +COQC bedrock2/bedrock2/src/Variables.v +COQC bedrock2/deps/riscv-coq/src/Utility/runsToNonDet.v +COQC bedrock2/deps/riscv-coq/src/Utility/ZBitOps.v +COQC bedrock2/bedrock2/src/StringNamesSyntax.v +COQC bedrock2/bedrock2/src/Bytedump.v +COQC bedrock2/bedrock2/src/Memory.v +COQC bedrock2/deps/riscv-coq/src/Utility/Utility.v +COQC bedrock2/deps/riscv-coq/src/Utility/prove_Zeq_bitwise.v +COQC bedrock2/bedrock2/src/Map/Separation.v +COQC bedrock2/bedrock2/src/StructNotations.v +COQC bedrock2/deps/riscv-coq/src/Utility/Words32Naive.v +COQC bedrock2/bedrock2/src/ToCString.v +COQC bedrock2/deps/riscv-coq/src/Utility/Words64Naive.v +COQC bedrock2/bedrock2/src/BytedumpTest.v +COQC bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl32.v + +
!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ +COQC bedrock2/bedrock2/src/Semantics.v +COQC bedrock2/deps/riscv-coq/src/Spec/Decode.v +COQC bedrock2/bedrock2/src/Map/SeparationLogic.v +COQC bedrock2/deps/riscv-coq/src/Platform/Memory.v +COQC bedrock2/deps/riscv-coq/src/Spec/Machine.v +COQC bedrock2/bedrock2/src/WeakestPrecondition.v +COQC bedrock2/deps/riscv-coq/src/Platform/RiscvMachine.v +COQC bedrock2/bedrock2/src/Array.v +COQC bedrock2/deps/riscv-coq/src/Utility/MkMachineWidth.v +COQC bedrock2/deps/riscv-coq/src/Spec/VirtualMemory.v +COQC bedrock2/bedrock2/src/BasicC64Syntax.v +COQC bedrock2/deps/riscv-coq/src/Platform/MetricRiscvMachine.v +COQC bedrock2/bedrock2/src/Examples/Trace.v +COQC bedrock2/deps/riscv-coq/src/Spec/ExecuteM.v +COQC bedrock2/deps/riscv-coq/src/Spec/ExecuteM64.v +squarer_correct + : forall (m : Semantics.mem) (l : Semantics.locals), + exec map.empty squarer [] m l + (fun (t' : trace) (_ : Semantics.mem) (_ : Semantics.locals) => + squarer_trace t') +squarer_correct + : forall (m : Semantics.mem) (l : Semantics.locals), + exec map.empty squarer [] m l + (fun (t' : trace) (_ : Semantics.mem) (_ : Semantics.locals) => + squarer_trace t') +COQC bedrock2/bedrock2/src/Examples/StructAccess.v +COQC bedrock2/deps/riscv-coq/src/Spec/PseudoInstructions.v +COQC bedrock2/bedrock2/src/BasicCSyntax.v +COQC bedrock2/deps/riscv-coq/src/Utility/InstructionCoercions.v +COQC bedrock2/bedrock2/src/WeakestPreconditionFile "bedrock2/deps/riscv-coq/src/Utility/InstructionCoercions.v", line 10, characters 0-70: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope ilist_scope.". [undeclared-scope,deprecated] +bedrock2/deps/riscv-coq/src/Utility/InstructionCoercions (real: 1.33, user: 0.43, sys: 0.21, mem: 313976 ko) +bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl64 (real: 1.59, user: 0.52, sys: 0.25, mem: 375840 ko) +bedrock2/deps/riscv-coq/src/Utility/Encode (real: 2.03, user: 0.67, sys: 0.31, mem: 446648 ko) +bedrock2/deps/riscv-coq/src/Spec/Primitives (real: 2.21, user: 0.72, sys: 0.34, mem: 457772 ko) +bedrock2/deps/riscv-coq/src/Spec/ExecuteI (real: 2.60, user: 0.94, sys: 0.32, mem: 454504 ko) +bedrock2/deps/riscv-coq/src/Spec/ExecuteI64 (real: 1.85, user: 0.55, sys: 0.28, mem: 401008 ko) +bedrock2/deps/riscv-coq/src/Spec/MetricPrimitives (real: 2.20, user: 0.76, sys: 0.30, mem: 459200 ko) +bedrock2/deps/riscv-coq/src/Spec/Execute (real: 1.43, user: 0.44, sys: 0.24, mem: 336624 ko) +bedrock2/deps/riscv-coq/src/Utility/InstructionNotations (real: 1.41, user: 0.44, sys: 0.24, mem: 340268 ko) +bedrock2/deps/riscv-coq/src/Platform/Run (real: 1.69, user: 0.52, sys: 0.27, mem: 374676 ko) +File "bedrock2/bedrock2/src/WeakestPreconditionProperties.v", line 193, characters 2-41: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +bedrock2/bedrock2/src/WeakestPreconditionProperties (real: 19.56, user: 9.19, sys: 0.41, mem: 663884 ko) +bedrock2/bedrock2/src/FE310CSemantics (real: 8.23, user: 3.64, sys: 0.34, mem: 472892 ko) +File "bedrock2/bedrock2/src/TailRecursion.v", line 16, characters 2-67: +Warning: Notation "_ /\ _" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/bedrock2/src/TailRecursion.v", line 47, characters 2-14: +Warning: Notation "_ * _" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/bedrock2/src/TailRecursion.v", line 47, characters 2-14: +Warning: Notation "{ _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/bedrock2/src/TailRecursion.v", line 47, characters 2-14: +Warning: Notation "{ _ : _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/bedrock2/src/TailRecursion.v", line 47, characters 2-14: +Warning: Notation "{ ' _ : _ & _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "bedrock2/bedrock2/src/TailRecursion.v", line 47, characters 2-14: +Warning: Notation "( _ , _ , .. , _ )" was already used in scope core_scope. +[notation-overridden,parsing] +File "bedrock2/bedrock2/src/TailRecursion.v", line 138, characters 2-49: +Warning: Notation "_ * _" was already used in scope type_scope. +[notation-overridden,parsing] +bedrock2/bedrock2/src/TailRecursion (real: 3.43, user: 1.34, sys: 0.32, mem: 461368 ko) +bedrock2/deps/riscv-coq/src/Platform/Minimal (real: 14.97, user: 6.99, sys: 0.33, mem: 482444 ko) +File "bedrock2/bedrock2/src/ptsto_bytes.v", line 151, characters 6-173: +Warning: Unused introduction patterns: R IH [unused-intro-pattern,tactics] +File "bedrock2/bedrock2/src/ptsto_bytes.v", line 163, characters 6-132: +Warning: Unused introduction patterns: R IH [unused-intro-pattern,tactics] +bedrock2/bedrock2/src/ptsto_bytes (real: 4.33, user: 1.80, sys: 0.31, mem: 461200 ko) +bedrock2/bedrock2/src/Examples/MultipleReturnValues (real: 1.64, user: 0.54, sys: 0.23, mem: 310296 ko) +bedrock2/bedrock2/src/Examples/ARPResponder (real: 4.88, user: 2.06, sys: 0.33, mem: 465924 ko) +bedrock2/bedrock2/src/Examples/chacha20 (real: 3.11, user: 1.25, sys: 0.26, mem: 435736 ko) +Properties.v +COQC bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl64.v +COQC bedrock2/deps/riscv-coq/src/Utility/Encode.v +COQC bedrock2/deps/riscv-coq/src/Spec/Primitives.v +COQC bedrock2/deps/riscv-coq/src/Spec/ExecuteI.v +COQC bedrock2/deps/riscv-coq/src/Spec/ExecuteI64.v +COQC bedrock2/deps/riscv-coq/src/Spec/MetricPrimitives.v +COQC bedrock2/deps/riscv-coq/src/Spec/Execute.v +COQC bedrock2/deps/riscv-coq/src/Utility/InstructionNotations.v +COQC bedrock2/deps/riscv-coq/src/Platform/Run.v +COQC bedrock2/deps/riscv-coq/src/Platform/Minimal.v +COQC bedrock2/bedrock2/src/FE310CSemantics.v +COQC bedrock2/bedrock2/src/TailRecursion.v +COQC bedrock2/bedrock2/src/ptsto_bytes.v +COQC bedrock2/deps/riscv-coq/src/Platform/MinimalMMIO.v +COQC bedrock2/bedrock2/src/Examples/MultipleReturnValues.v +COQC bedrock2/bedrock2/src/Examples/ARPResponder.v +COQC bedrock2/bedrock2/src/Examples/chacha20.v +COQC bedrock2/bedrock2/src/Examples/Demos.v +allProgs@{bedrock2.Examples.Demos.686 bedrock2.Examples.Demos.687} = +[("bsearch", + ([left; right; target], [left], + (while (right - left) {{ + mid = left + (right - left) >> 4 << 3;; + (if (*(uintptr_t*) mid < target) {{ + left = mid + 8 + }} else {{ + right = mid + }});; + cmd.unset mid + }})%bedrock_cmd)); +("listsum", +([], [sumreg], +(sumreg = 0;; + n = *(uint32_t*) 1024;; + ListSum.i = 0;; + while (ListSum.i < n) {{ + ListSum.a = *(uint32_t*) (1024 + 4 + 4 * ListSum.i);; + sumreg = sumreg + ListSum.a;; + ListSum.i = ListSum.i + 1 + }})%bedrock_cmd)); +("fibonacci", +([], [b], +(a = 0;; + b = 1;; + i = 0;; + while (i < 6) {{ + c = a + b;; + a = b;; + b = c;; + i = i + 1 + }})%bedrock_cmd))] + : list Prog +allProgs@{bedrock2.Examples.Demos.135 bedrock2.Examples.Demos.136 +bedrock2.Examples.Demos.137 bedrock2.Examples.Demos.146 +bedrock2.Examples.Demos.171 bedrock2.Examples.Demos.345 +bedrock2.Examples.Demos.515 bedrock2.Examples.Demos.686 +bedrock2.Examples.Demos.687} = +fun (p : Syntax.parameters) (bsearchNames : BinarySearch.Names) + (listsumNames : ListSum.Names) (fibonacciNames : Fibonacci.Names) => +[("bsearch", + ([BinarySearch.left; BinarySearch.right; BinarySearch.target], + [BinarySearch.left], + cmd.while + (expr.op bopname.sub (var BinarySearch.right) (var BinarySearch.left)) + (cmd.seq + (cmd.set BinarySearch.mid + (expr.op bopname.add (var BinarySearch.left) + (expr.op bopname.slu + (expr.op bopname.sru + (expr.op bopname.sub (var BinarySearch.right) + (var BinarySearch.left)) (literal 4)) + (literal 3)))) + (cmd.seq + (cmd.cond + (expr.op bopname.ltu + (expr.load access_size.word (var BinarySearch.mid)) + (var BinarySearch.target)) + (cmd.set BinarySearch.left + (expr.op bopname.add (var BinarySearch.mid) (literal 8))) + (cmd.set BinarySearch.right (var BinarySearch.mid))) + (cmd.unset BinarySearch.mid))))); +("listsum", +([], [ListSum.sumreg], +cmd.seq (cmd.set ListSum.sumreg (literal 0)) + (cmd.seq (cmd.set ListSum.n (expr.load access_size.four (literal 1024))) + (cmd.seq (cmd.set ListSum.i (literal 0)) + (cmd.while (expr.op bopname.ltu (var ListSum.i) (var ListSum.n)) + (cmd.seq + (cmd.set ListSum.a + (expr.load access_size.four + (expr.op bopname.add (literal (1024 + 4)) + (expr.op bopname.mul (literal 4) (var ListSum.i))))) + (cmd.seq + (cmd.set ListSum.sumreg + (expr.op bopname.add (var ListSum.sumreg) (var ListSum.a))) + bedrock2/bedrock2/src/Examples/Demos (real: 1.93, user: 0.69, sys: 0.23, mem: 353168 ko) +bedrock2/bedrock2/src/BasicC32Semantics (real: 1.66, user: 0.55, sys: 0.25, mem: 387552 ko) +bedrock2/bedrock2/src/BasicC64Semantics (real: 1.74, user: 0.57, sys: 0.27, mem: 403188 ko) +bedrock2/bedrock2/src/Scalars (real: 3.04, user: 1.18, sys: 0.30, mem: 457564 ko) +bedrock2/bedrock2/src/TODO_absint (real: 2.93, user: 1.13, sys: 0.30, mem: 457912 ko) + (cmd.set ListSum.i + (expr.op bopname.add (var ListSum.i) (literal 1)))))))))); +("fibonacci", +([], [Fibonacci.b], +cmd.seq (cmd.set Fibonacci.a (literal 0)) + (cmd.seq (cmd.set Fibonacci.b (literal 1)) + (cmd.seq (cmd.set Fibonacci.i (literal 0)) + (cmd.while (expr.op bopname.ltu (var Fibonacci.i) (literal 6)) + (cmd.seq + (cmd.set Fibonacci.c + (expr.op bopname.add (var Fibonacci.a) (var Fibonacci.b))) + (cmd.seq (cmd.set Fibonacci.a (var Fibonacci.b)) + (cmd.seq (cmd.set Fibonacci.b (var Fibonacci.c)) + (cmd.set Fibonacci.i + (expr.op bopname.add (var Fibonacci.i) (literal 1)))))))))))] + : forall p : Syntax.parameters, + BinarySearch.Names -> ListSum.Names -> Fibonacci.Names -> list Prog + +Arguments p, bsearchNames, listsumNames, fibonacciNames are implicit and +maximally inserted +allProgsAsCStrings@{} = +["uintptr_t bsearch(uintptr_t left, uintptr_t right, uintptr_t target) { + uintptr_t mid; + while ((right)-(left)) { + mid = (left)+((((right)-(left))>>((uintptr_t)4ULL))<<((uintptr_t)3ULL)); + if ((*(uintptr_t*)(mid))<(target)) { + left = (mid)+((uintptr_t)8ULL); + } else { + right = mid; + } + // unset mid + } + return left; +} +"; +"uintptr_t listsum() { + uintptr_t n, sumreg, a, i; + sumreg = (uintptr_t)0ULL; + n = *(uint32_t*)((uintptr_t)1024ULL); + i = (uintptr_t)0ULL; + while ((i)<(n)) { + a = *(uint32_t*)(((uintptr_t)1028ULL)+(((uintptr_t)4ULL)*(i))); + sumreg = (sumreg)+(a); + i = (i)+((uintptr_t)1ULL); + } + return sumreg; +} +"; +"uintptr_t fibonacci() { + uintptr_t a, b, c, i; + a = (uintptr_t)0ULL; + b = (uintptr_t)1ULL; + i = (uintptr_t)0ULL; + while ((i)<((uintptr_t)6ULL)) { + c = (a)+(b); + a = b; + b = c; + i = (i)+((uintptr_t)1ULL); + } + return b; +} +"] + : list string +allProgsWithZNames@{bedrock2.Examples.Demos.721} = +[("bsearch", + ([1; 2; 3], [1], + cmd.while (expr.op bopname.sub (expr.var 2) (expr.var 1)) + (cmd.seq + (cmd.set 4 + (expr.op bopname.add (expr.var 1) + (expr.op bopname.slu + (expr.op bopname.sru + (expr.op bopname.sub (expr.var 2) (expr.var 1)) + (expr.literal 4)) (expr.literal 3)))) + (cmd.seq + (cmd.cond + (expr.op bopname.ltu (expr.load access_size.word (expr.var 4)) + (expr.var 3)) + (cmd.set 1 (expr.op bopname.add (expr.var 4) (expr.literal 8))) + (cmd.set 2 (expr.var 4))) (cmd.unset 4))))); +("listsum", +([], [3], +cmd.seq (cmd.set 3 (expr.literal 0)) + (cmd.seq (cmd.set 1 (expr.load access_size.four (expr.literal 1024))) + (cmd.seq (cmd.set 2 (expr.literal 0)) + (cmd.while (expr.op bopname.ltu (expr.var 2) (expr.var 1)) + (cmd.seq + (cmd.set 4 + (expr.load access_size.four + (expr.op bopname.add (expr.literal 1028) + (expr.op bopname.mul (expr.literal 4) (expr.var 2))))) + (cmd.seq + (cmd.set 3 (expr.op bopname.add (expr.var 3) (expr.var 4))) + (cmd.set 2 + (expr.op bopname.add (expr.var 2) (expr.literal 1)))))))))); +("fibonacci", +([], [2], +cmd.seq (cmd.set 1 (expr.literal 0)) + (cmd.seq (cmd.set 2 (expr.literal 1)) + (cmd.seq (cmd.set 4 (expr.literal 0)) + (cmd.while (expr.op bopname.ltu (expr.var 4) (expr.literal 6)) + (cmd.seq + (cmd.set 3 (expr.op bopname.add (expr.var 1) (expr.var 2))) + (cmd.seq (cmd.set 1 (expr.var 2)) + (cmd.seq (cmd.set 2 (expr.var 3)) + (cmd.set 4 + (expr.op bopname.add (expr.var 4) (expr.literal 1)))))))))))] + : list (string * (list Z * list Z * cmd)) +COQC bedrock2/bedrock2/src/BasicC32Semantics.v +COQC bedrock2/bedrock2/src/BasicC64Semantics.v +COQC bedrock2/bedrock2/src/Scalars.v +COQC bedrock2/bedrock2/src/TODO_absint.v +bedrock2/bedrock2/src/ProgramLogic (real: 1.65, user: 0.52, sys: 0.25, mem: 371960 ko) +File "bedrock2/bedrock2/src/Examples/lightbulb.v", line 48, characters 0-36: +Warning: Notation "_ * _" was already used in scope type_scope. +[notation-overridden,parsing] +bedrock2/bedrock2/src/Examples/lightbulb (real: 44.98, user: 21.59, sys: 0.37, mem: 525428 ko) +File "bedrock2/bedrock2/src/Examples/swap.v", line 31, characters 24-60: +Warning: Notation "_ * _" was already used in scope type_scope. +[notation-overridden,parsing] +bedrock2/bedrock2/src/Examples/swap (real: 8.68, user: 3.88, sys: 0.33, mem: 478956 ko) +bedrock2/deps/riscv-coq/src/Platform/MinimalMMIO (real: 140.04, user: 67.92, sys: 0.50, mem: 590104 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_Fence (real: 19.81, user: 9.16, sys: 0.36, mem: 495544 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R (real: 13.71, user: 6.32, sys: 0.36, mem: 478812 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R_atomic (real: 18.82, user: 8.68, sys: 0.36, mem: 494004 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I (real: 14.67, user: 6.82, sys: 0.30, mem: 485168 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_57 (real: 13.83, user: 6.36, sys: 0.32, mem: 478692 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_66 (real: 40.12, user: 19.20, sys: 0.36, mem: 526372 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_system (real: 10.48, user: 4.71, sys: 0.33, mem: 470712 ko) +bedrock2/bedrock2/src/Examples/bsearch (real: 208.32, user: 101.50, sys: 0.51, mem: 564436 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_S (real: 25.56, user: 12.11, sys: 0.34, mem: 518652 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_SB (real: 55.25, user: 26.55, sys: 0.40, mem: 632108 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_U (real: 9.99, user: 4.46, sys: 0.31, mem: 468412 ko) +bedrock2/bedrock2/src/Examples/FE310CompilerDemo (real: 83.94, user: 40.64, sys: 0.41, mem: 588832 ko) +bedrock2/bedrock2/src/Examples/ipow (real: 19.97, user: 9.35, sys: 0.30, mem: 496100 ko) +/bin/sh: 1: hexdump: not found +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_UJ (real: 39.56, user: 19.19, sys: 0.35, mem: 580040 ko) +bedrock2/deps/riscv-coq/src/Proofs/invert_encode_FenceI (real: 14.48, user: 6.72, sys: 0.31, mem: 485544 ko) +bedrock2/deps/riscv-coq/src/Utility/runsToNonDet_Run (real: 1.66, user: 0.58, sys: 0.23, mem: 408744 ko) +bedrock2/deps/riscv-coq/src/Platform/MinimalLogging (real: 2.10, user: 0.74, sys: 0.27, mem: 460380 ko) +bedrock2/deps/riscv-coq/src/Platform/MetricMinimal (real: 24.74, user: 11.74, sys: 0.31, mem: 501100 ko) +COQC bedrock2/bedrock2/src/ProgramLogic.v +COQC bedrock2/bedrock2/src/Examples/lightbulb.v + = "uintptr_t lightbulb(uintptr_t packet, uintptr_t len) { + uintptr_t ethertype, protocol, mmio_val, command, r; + ethertype = ((*(uint8_t*)((packet)+((uintptr_t)12ULL)))<<((uintptr_t)8ULL))|(*(uint8_t*)((packet)+((uintptr_t)13ULL))); + if (((uintptr_t)1535ULL)<(ethertype)) { + protocol = *(uint8_t*)((packet)+((uintptr_t)23ULL)); + if ((protocol)==((uintptr_t)17ULL)) { + command = *(uint8_t*)((packet)+((uintptr_t)42ULL)); + mmio_val = MMIOREAD((uintptr_t)268509192ULL); + MMIOWRITE((uintptr_t)268509192ULL, (mmio_val)|(((uintptr_t)1ULL)<<((uintptr_t)23ULL))); + mmio_val = MMIOREAD((uintptr_t)268509196ULL); + MMIOWRITE((uintptr_t)268509196ULL, (mmio_val)|((command)<<((uintptr_t)23ULL))); + r = (uintptr_t)0ULL; + } else { + r = (uintptr_t)-1ULL; + } + } else { + r = (uintptr_t)-1ULL; + } + return r; +} +" + : string +COQC bedrock2/bedrock2/src/Examples/swap.v +static void swap(uintptr_t a, uintptr_t b); + +void swap_swap(uintptr_t a, uintptr_t b) { + swap(a, b); + swap(a, b); + return; +} + +static void swap(uintptr_t a, uintptr_t b) { + uintptr_t t; + t = *(uintptr_t*)(b); + *(uintptr_t*)(b) = *(uintptr_t*)(a); + *(uintptr_t*)(a) = t; + return; +} + +COQC bedrock2/bedrock2/src/Examples/bsearch.v +H19 +H13 +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_Fence.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R_atomic.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_57.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_66.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_system.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_S.v +COQC bedrock2/bedrock2/src/Examples/FE310CompilerDemo.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_SB.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_U.v +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_UJ.v +COQC bedrock2/bedrock2/src/Examples/ipow.v +make[3]: Leaving directory 'bedrock2/bedrock2' +make src/BytedumpTest.out +make[3]: Entering directory 'bedrock2/bedrock2' +coqc -q -Q src bedrock2 -Q bedrock2/deps/coqutil/src coqutil src/BytedumpTest.v | head --bytes -1 > src/BytedumpTest.out.tmp +hexdump < /dev/null && \ + hexdump -C src/BytedumpTest.golden.bin > src/BytedumpTest.golden.hex && \ + hexdump -C src/BytedumpTest.out.tmp > src/BytedumpTest.out.hex && \ + diff -u src/BytedumpTest.golden.hex src/BytedumpTest.out.hex && \ + rm src/BytedumpTest.golden.hex src/BytedumpTest.out.hex || true +diff -u src/BytedumpTest.golden.bin src/BytedumpTest.out.tmp +mv src/BytedumpTest.out.tmp src/BytedumpTest.out +make[3]: Leaving directory 'bedrock2/bedrock2' +make[2]: Leaving directory 'bedrock2/bedrock2' +COQC bedrock2/deps/riscv-coq/src/Proofs/invert_encode_FenceI.v +COQC bedrock2/deps/riscv-coq/src/Proofs/EncodeBound.v +COQC bedrock2/deps/riscv-coq/src/Utility/runsToNonDet_Run.v +COQC bedrock2/deps/riscv-coq/src/Platform/MinimalLogging.v +COQC bedrock2/deps/riscv-coq/src/Platform/MetricMinimal.v +COQC bedrock2/deps/riscv-coq/src/Platform/Example.v + = [({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 36 (IInstruction (Blt 9 19 (-16))), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 32 (IInstruction (Addi 9 9 1)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 28 (IInstruction (Addi 18 21 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 24 (IInstruction (Addi 20 18 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 20 (IInstruction (Add 21 20 18)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 36 (IInstruction (Blt 9 19 (-16))), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 32 (IInstruction (Addi 9 9 1)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 28 (IInstruction (Addi 18 21 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 24 (IInstruction (Addi 20 18 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 20 (IInstruction (Add 21 20 18)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 36 (IInstruction (Blt 9 19 (-16))), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 32 (IInstruction (Addi 9 9 1)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 28 (IInstruction (Addi 18 21 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 24 (IInstruction (Addi 20 18 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 20 (IInstruction (Add 21 20 18)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 36 (IInstruction (Blt 9 19 (-16))), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 32 (IInstruction (Addi 9 9 1)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 28 (IInstruction (Addi 18 21 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 24 (IInstruction (Addi 20 18 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 20 (IInstruction (Add 21 20 18)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 36 (IInstruction (Blt 9 19 (-16))), [], + ({| SortedList.value := []; Sbedrock2/deps/riscv-coq/src/Platform/Example (real: 4.13, user: 1.62, sys: 0.27, mem: 468188 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeProver (real: 2.54, user: 0.94, sys: 0.29, mem: 450352 ko) +bedrock2/deps/riscv-coq/src/Platform/Example64Literal (real: 2.12, user: 0.76, sys: 0.28, mem: 409784 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA64 (real: 55.42, user: 26.45, sys: 0.45, mem: 605916 ko) +bedrock2/deps/riscv-coq/src/Proofs/EncodeBound (real: 103.45, user: 50.15, sys: 0.41, mem: 573560 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI64 (real: 53.82, user: 25.80, sys: 0.43, mem: 650288 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA (real: 60.04, user: 28.68, sys: 0.44, mem: 639092 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeCSR (real: 215.18, user: 104.22, sys: 0.79, mem: 997556 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM64 (real: 21.95, user: 9.77, sys: 0.34, mem: 523092 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM (real: 47.35, user: 22.60, sys: 0.37, mem: 589708 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI (real: 226.75, user: 139.56, sys: 1.26, mem: 1730872 ko) +bedrock2/deps/riscv-coq/src/Proofs/DecodeEncode (real: 0.81, user: 0.42, sys: 0.18, mem: 374624 ko) +ortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 32 (IInstruction (Addi 9 9 1)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 28 (IInstruction (Addi 18 21 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 24 (IInstruction (Addi 20 18 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 20 (IInstruction (Add 21 20 18)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 36 (IInstruction (Blt 9 19 (-16))), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 32 (IInstruction (Addi 9 9 1)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 28 (IInstruction (Addi 18 21 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 24 (IInstruction (Addi 20 18 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 20 (IInstruction (Add 21 20 18)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 36 (IInstruction (Blt 9 19 (-16))), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 16 (IInstruction (Jal 0 20)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 12 (IInstruction (Addi 9 0 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 8 (IInstruction (Addi 18 0 1)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 4 (IInstruction (Addi 20 0 0)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, [])); + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, + EvLoadWord 0 (IInstruction (Addi 19 0 6)), [], + ({| SortedList.value := []; SortedList._value_ok := eq_refl |}, []))] + : list (LogItem LogEvent) +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeProver.v +COQC bedrock2/deps/riscv-coq/src/Platform/Example64Literal.v + = {| unsigned := 1073745919; _unsigned_in_range := eq_refl |} + : word64 +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA64.v +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeCSR.v +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI64.v +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA.v +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI.v +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM64.v +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM.v +COQC bedrock2/deps/riscv-coq/src/Proofs/DecodeEncode.v +make[3]: Leaving directory 'bedrock2/deps/riscv-coq' +make[2]: Leaving directory 'bedrock2/deps/riscv-coq' +make -C bedrock2/compiler +make -C bedrock2/deps/kami +make[2]: Entering directory 'bedrock2/compiler' +printf -- '-Q ../bedrock2/src bedrock2\n-Q bedrock2/deps/coqutil/src coqutil\n-Q bedrock2/deps/riscv-coq/src riscv\n-Q ./lib lib\n-Q ./src compiler\n' > _CoqProject +/builds/coq/coq/_install_ci/bin/coq_makefile -f _CoqProject INSTALLDEFAULTROOT = bedrock2 -arg "-async-proofs-tac-j 1" bedrock2/compiler/src/EmitsValid.v bedrock2/compiler/src/util/Misc.v bedrock2/compiler/src/util/Learning.v bedrock2/compiler/src/util/Tactics.v bedrock2/compiler/src/util/MyOmega.v bedrock2/compiler/src/util/ListLib.v bedrock2/compiler/src/util/Set.v bedrock2/compiler/src/util/SetSolverTests.v bedrock2/compiler/src/util/Common.v bedrock2/compiler/src/util/LogGoal.v bedrock2/compiler/src/SeparationLogic.v bedrock2/compiler/src/ExprImp.v bedrock2/compiler/src/FlatToRiscv32.v bedrock2/compiler/src/FlatToRiscv.v bedrock2/compiler/src/on_hyp_containing.v bedrock2/compiler/src/Basic32Semantics.v bedrock2/compiler/src/Simp.v bedrock2/compiler/src/FlatToRiscvDef.v bedrock2/compiler/src/RegAlloc3.v bedrock2/compiler/src/RegAllocAnnotatedNotations.v bedrock2/compiler/src/UnmappedMemForExtSpec.v bedrock2/compiler/src/RegAlloc2.v bedrock2/compiler/src/NoActionSyntaxParams.v bedrock2/compiler/src/Pipeline.v bedrock2/compiler/src/RiscvWordProperties.v bedrock2/compiler/src/GoFlatToRiscv.v bedrock2/compiler/src/Rem4.v bedrock2/compiler/src/SimplWordExpr.v bedrock2/compiler/src/ZNameGen.v bedrock2/compiler/src/NameGen.v bedrock2/compiler/src/FlatImp.v bedrock2/compiler/src/FlattenExpr.v bedrock2/compiler/src/eqexact.v bedrock2/compiler/src/examples/swap_bytes_over_uart_hexdump.v bedrock2/compiler/src/examples/TestExprImp.v bedrock2/compiler/src/examples/highlevel/FuncMut.v bedrock2/compiler/src/examples/highlevel/For.v bedrock2/compiler/src/examples/InlineAssemblyMacro.v bedrock2/compiler/src/examples/CompileExamples.v bedrock2/compiler/src/examples/toposort.v bedrock2/compiler/src/examples/FE310Compiler.v bedrock2/compiler/src/examples/EditDistExample.v bedrock2/compiler/src/examples/Fibonacci.v bedrock2/compiler/src/examples/TestFlatImp.v bedrock2/compiler/src/examples/MMIO.v bedrock2/compiler/lib/LibTacticsMin.v bedrock2/compiler/lib/fiat_crypto_tactics/Not.v bedrock2/compiler/lib/fiat_crypto_tactics/Test.v bedrock2/compiler/lib/fiat_crypto_tactics/UniquePose.v bedrock2/compiler/lib/LibTactics.v -o Makefile.coq.all +make[2]: Entering directory 'bedrock2/deps/kami' +printf -- '-R Kami Kami\n-Q bedrock2/deps/Warning: ../bedrock2/src (used in -R or -Q) is not a subdirectory of the current directory + +Warning: bedrock2/deps/riscv-coq/src (used in -R or -Q) is not a subdirectory of the current directory + +Warning: no common logical root +Warning: in such case INSTALLDEFAULTROOT must be defined +Warning: the install-doc target is going to install files +Warning: in orphan_riscv_coqutil_Kami +bedrock2/compiler/lib/fiat_crypto_tactics/Test (real: 0.17, user: 0.04, sys: 0.04, mem: 55660 ko) +File "bedrock2/compiler/lib/LibTacticsMin.v", line 76, characters 0-32: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "bedrock2/compiler/lib/LibTacticsMin.v", line 121, characters 0-42: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope ltac_scope.". [undeclared-scope,deprecated] +File "bedrock2/compiler/lib/LibTacticsMin.v", line 463, characters 0-16: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +bedrock2/compiler/lib/LibTacticsMin (real: 0.92, user: 0.31, sys: 0.14, mem: 301996 ko) +bedrock2/compiler/src/NoActionSyntaxParams (real: 0.17, user: 0.04, sys: 0.03, mem: 57364 ko) +bedrock2/compiler/lib/fiat_crypto_tactics/UniquePose (real: 0.16, user: 0.04, sys: 0.03, mem: 57340 ko) +File "./Kami/Lib/StringAsOT.v", line 86, characters 2-38: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Lib/StringAsOT (real: 1.80, user: 0.70, sys: 0.19, mem: 423260 ko) +bedrock2/compiler/src/Simp (real: 1.02, user: 0.36, sys: 0.13, mem: 298624 ko) +bedrock2/compiler/src/util/Misc (real: 0.19, user: 0.05, sys: 0.04, mem: 70976 ko) +bedrock2/compiler/src/util/Learning (real: 0.16, user: 0.04, sys: 0.03, mem: 58420 ko) +File "./Kami/Lib/CommonTactics.v", line 276, characters 0-39: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/CommonTactics.v", line 277, characters 0-92: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Lib/CommonTactics (real: 1.03, user: 0.38, sys: 0.13, mem: 319992 ko) +bedrock2/compiler/src/util/MyOmega (real: 0.97, user: 0.33, sys: 0.14, mem: 289700 ko) +bedrock2/compiler/src/util/LogGoal (real: 0.15, user: 0.03, sys: 0.03, mem: 54716 ko) +Kami/Lib/StringEq (real: 1.50, user: 0.55, sys: 0.18, mem: 413664 ko) +File "bedrock2/compiler/src/SeparationLogic.v", line 10, characters 0-29: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope sep_scope.". [undeclared-scope,deprecated] +bedrock2/compiler/src/SeparationLogic (real: 1.37, user: 0.48, sys: 0.16, mem: 352200 ko) +Kami/Lib/Nomega (real: 1.17, user: 0.38, sys: 0.19, mem: 363832 ko) +Kami/Lib/DepEq (real: 0.46, user: 0.14, sys: 0.08, mem: 160816 ko) +Kami/Lib/VectorFacts (real: 0.56, user: 0.17, sys: 0.09, mem: 180940 ko) +bedrock2/compiler/src/Rem4 (real: 1.86, user: 0.68, sys: 0.21, mem: 447424 ko) +bedrock2/compiler/src/SimplWordExpr (real: 1.85, user: 0.67, sys: 0.22, mem: 446424 ko) +Kami/Lib/StringAsList (real: 2.62, user: 1.08, sys: 0.20, mem: 421756 ko) +Kami/Lib/FinNotations (real: 0.43, user: 0.13, sys: 0.07, mem: 142092 ko) +bedrock2/compiler/src/RiscvWordProperties (real: 1.24, user: 0.43, sys: 0.18, mem: 362292 ko) +bedrock2/compiler/src/eqexact (real: 0.15, user: 0.04, sys: 0.03, mem: 56364 ko) +bedrock2/compiler/src/on_hyp_containing (real: 0.15, user: 0.04, sys: 0.03, mem: 56680 ko) +Kami/Lib/Reflection (real: 1.00, user: 0.34, sys: 0.15, mem: 328692 ko) +Kami/Lib/Concat (real: 1.06, user: 0.36, sys: 0.16, mem: 338456 ko) +bedrock2/compiler/src/Basic32Semantics (real: 1.46, user: 0.50, sys: 0.20, mem: 385968 ko) +riscv-coq/src riscv\n-Q bedrock2/deps/coqutil/src coqutil\n' > _CoqProject +make -f Makefile.coq.all +make[3]: Entering directory 'bedrock2/compiler' +/builds/coq/coq/_install_ci/bin/coq_makefile -f _CoqProject Kami/Lib/StringStringAsOT.v Kami/Lib/FMap.v Kami/Lib/ilist.v Kami/Lib/Indexer.v Kami/Lib/DepEq.v Kami/Lib/Nomega.v Kami/Lib/StringEq.v Kami/Lib/Misc.v Kami/Lib/Word.v Kami/Lib/FinNotations.v Kami/Lib/Reflection.v Kami/Lib/NatLib.v Kami/Lib/StringAsList.v Kami/Lib/Concat.v Kami/Lib/ListSupport.v Kami/Lib/VectorFacts.v Kami/Lib/StringAsOT.v Kami/Lib/CommonTactics.v Kami/Lib/WordSupport.v Kami/Lib/BasicLogic.v Kami/Lib/DepEqNat.v Kami/Lib/Struct.v Kami/SemFacts.v Kami/ParametricInlineLtac.v Kami/PartialInlineFacts.v Kami/Wf.v Kami/Semantics.v Kami/ParametricSyntax.v Kami/Inline.v Kami/StepDet.v Kami/InlineFacts.v Kami/Amortization.v Kami/Tutorial.v Kami/Label.v Kami/MapReifyEx.v Kami/ParametricEquiv.v Kami/ParametricInline.v Kami/Notations.v Kami/Substitute.v Kami/ParametricWf.v Kami/ParamDup.v Kami/SymEval.v Kami/Syntax.v Kami/ModuleBoundEx.v Kami/Tactics.v Kami/SymEvalTac.v Kami/ModularFacts.v Kami/Synthesize.v Kami/RefinementFacts.v Kami/Decomposition.v Kami/Renaming.v Kami/Kami.v Kami/Duplicate.v Kami/ModuleBound.v Kami/Specialize.v Kami/Ex/ProcThreeStage.v Kami/Ex/SimpleFifoCorrect.v Kami/Ex/IsaRv32PgmExt.v Kami/Ex/ProcThreeStInv.v Kami/Ex/Divider32.v Kami/Ex/SC.v Kami/Ex/Names.v Kami/Ex/OneEltFifo.v Kami/Ex/Multiplier64.v Kami/Ex/Multiplier32.v Kami/Ex/ProcFDInv.v Kami/Ex/ProcDec.v Kami/Ex/ProcFourStDec.v Kami/Ex/IsaRv32.v Kami/Ex/MemAtomic.v Kami/Ex/ProcFDInl.v Kami/Ex/IsaRv32Pgm.v Kami/Ex/Divider64.v Kami/Ex/Fifo.v Kami/Ex/ProcThreeStInl.v Kami/Ex/ProcDecSC.v Kami/Ex/ProcDecSCN.v Kami/Ex/NativeFifo.v Kami/Ex/FifoCorrect.v Kami/Ex/ProcThreeStDec.v Kami/Ex/RegFile.v Kami/Ex/InDepthTutorial.v Kami/Ex/ProcDecInv.v Kami/Ex/ProcFetchDecode.v Kami/Ex/SCMMInl.v Kami/Ex/ProcFDCorrect.v Kami/Ex/MemTypes.v Kami/Ex/ProcDecInl.v Kami/Ex/IsaRv32/PgmFact.v Kami/Ex/IsaRv32/PgmMatMulReport.v Kami/Ex/IsaRv32/PgmBankerWorker3.v Kami/Ex/IsaRv32/PgmGcd.v Kami/Ex/IsaRv32/PgmMatMulInit.v Kami/Ex/IsaRv32/PgmPeterson2.v Kami/Ex/IsaRv32/PgmHanoi.v Kami/Ex/IsaRv32/PgmBankerWorker1.v Kami/Ex/IsaRv32/PgmPeterson1.v Kami/Ex/IsaRv32/PgmBankerInit.v Kami/Ex/IsaRv32/PgmMatMulNormal1.v Kami/Ex/IsaRv32/PgmDekker1.v Kami/Ex/IsaRv32/PgmBankerWorker2.v Kami/Ex/IsaRv32/PgmBsort.v Kami/Ex/IsaRv32/PgmMatMulNormal2.v Kami/Ex/IsaRv32/PgmDekker2.v Kami/Ext/Extraction.v Kami/Ext/BSyntax.v -o Makefile.coq.all +make -f Makefile.coq.all +make[3]: Entering directory 'bedrock2/deps/kami' +COQDEP VFILES +COQDEP VFILES +COQC bedrock2/compiler/lib/fiat_crypto_tactics/Test.v +COQC bedrock2/compiler/lib/LibTacticsMin.v +COQC Kami/Lib/StringAsOT.v +COQC bedrock2/compiler/src/NoActionSyntaxParams.v +COQC bedrock2/compiler/lib/fiat_crypto_tactics/UniquePose.v +COQC bedrock2/compiler/src/Simp.v +COQC Kami/Lib/CommonTactics.v +COQC bedrock2/compiler/src/util/Misc.v +COQC bedrock2/compiler/src/util/Learning.v +COQC bedrock2/compiler/src/util/MyOmega.v +COQC Kami/Lib/StringEq.v +COQC bedrock2/compiler/src/util/LogGoal.v +COQC bedrock2/compiler/src/SeparationLogic.v +COQC Kami/Lib/Nomega.v +COQC bedrock2/compiler/src/Rem4.v +COQC Kami/Lib/DepEq.v +COQC Kami/Lib/VectorFacts.v +COQC Kami/Lib/StringAsList.v +COQC bedrock2/compiler/src/SimplWordExpr.v +COQC bedrock2/compiler/src/RiscvWordProperties.v +COQC Kami/Lib/FinNotations.v +COQC Kami/Lib/Reflection.v +COQC bedrock2/compiler/src/eqexact.v +COQC bedrock2/compiler/src/on_hyp_containing.v +COQC bedrock2/compiler/src/Basic32Semantics.v +COQC Kami/Lib/Concat.v +COQC Kami/LKami/Lib/ListSupport (real: 1.09, user: 0.37, sys: 0.15, mem: 353524 ko) +File "bedrock2/compiler/src/UnmappedMemForExtSpec.v", line 45, characters 2-49: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "bedrock2/compiler/src/UnmappedMemForExtSpec.v", line 47, characters 2-30: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Lib/BasicLogic (real: 0.24, user: 0.07, sys: 0.03, mem: 87856 ko) +Kami/Lib/DepEqNat (real: 0.22, user: 0.06, sys: 0.03, mem: 76484 ko) +bedrock2/compiler/src/UnmappedMemForExtSpec (real: 1.68, user: 0.61, sys: 0.21, mem: 446012 ko) +Kami/Ex/Names (real: 1.02, user: 0.36, sys: 0.13, mem: 271052 ko) +bedrock2/compiler/src/NameGen (real: 0.95, user: 0.32, sys: 0.15, mem: 286108 ko) +bedrock2/compiler/src/examples/highlevel/For (real: 0.15, user: 0.04, sys: 0.02, mem: 55764 ko) +Kami/Lib/StringStringAsOT (real: 1.73, user: 0.63, sys: 0.19, mem: 420276 ko) +bedrock2/compiler/src/examples/toposort (real: 2.47, user: 0.98, sys: 0.21, mem: 426872 ko) +File "bedrock2/compiler/lib/LibTactics.v", line 55, characters 0-32: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "bedrock2/compiler/lib/LibTactics.v", line 100, characters 0-42: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope ltac_scope.". [undeclared-scope,deprecated] +File "bedrock2/compiler/lib/LibTactics.v", line 581, characters 0-16: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "bedrock2/compiler/lib/LibTactics.v", line 4771, characters 0-28: +Warning: skip_axiom is declared as a local axiom [local-declaration,scope] +File "bedrock2/compiler/lib/LibTactics.v", line 4998, characters 0-196: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope let_scope.". [undeclared-scope,deprecated] +Kami/Lib/NatLib (real: 3.58, user: 1.52, sys: 0.22, mem: 429812 ko) +bedrock2/compiler/lib/LibTactics (real: 2.73, user: 1.10, sys: 0.23, mem: 419492 ko) +bedrock2/compiler/lib/fiat_crypto_tactics/Not (real: 0.17, user: 0.05, sys: 0.03, mem: 56680 ko) +bedrock2/compiler/src/util/Tactics (real: 1.16, user: 0.40, sys: 0.17, mem: 282384 ko) +Kami/Lib/ilist (real: 2.17, user: 0.82, sys: 0.23, mem: 422368 ko) +bedrock2/compiler/src/util/Common (real: 1.69, user: 0.59, sys: 0.22, mem: 371952 ko) +Kami/Lib/Indexer (real: 2.29, user: 0.90, sys: 0.21, mem: 421100 ko) +bedrock2/compiler/src/util/ListLib (real: 2.24, user: 0.88, sys: 0.22, mem: 427540 ko) +Kami/Lib/Misc (real: 1.05, user: 0.35, sys: 0.16, mem: 299684 ko) +bedrock2/compiler/src/util/Set (real: 0.96, user: 0.30, sys: 0.14, mem: 282580 ko) +File "./Kami/Lib/Word.v", line 19, characters 0-35: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope word_scope.". [undeclared-scope,deprecated] +File "./Kami/Lib/Word.v", line 147, characters 0-28: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/Word.v", line 400, characters 0-45: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/Word.v", line 1090, characters 0-43: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/Word.v", line 1217, characters 0-42: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "bedrock2/compiler/src/ExprImp.v", line 407, characters 4-639: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 407, characters 4-639: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 407, characters 4-639: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 407, characters 4-639: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 407, characters 4-639: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 407, characters 4-639: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 464, characters 4-57: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 464, characters 4-57: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 491, characters 4-95: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 491, characters 4-95: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 491, characters 4-95: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 533, characters 4-108: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 533, characters 4-108: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/ExprImp.v", line 533, characters 4-108: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +ib/ListSupport.v +COQC bedrock2/compiler/src/UnmappedMemForExtSpec.v +COQC Kami/Lib/BasicLogic.v +COQC Kami/Lib/DepEqNat.v +COQC Kami/Ex/Names.v +COQC bedrock2/compiler/src/NameGen.v +COQC Kami/Lib/StringStringAsOT.v +COQC bedrock2/compiler/src/examples/highlevel/For.v +COQC bedrock2/compiler/src/examples/toposort.v +COQC Kami/Lib/NatLib.v +COQC bedrock2/compiler/lib/LibTactics.v +COQC Kami/Lib/ilist.v +COQC bedrock2/compiler/lib/fiat_crypto_tactics/Not.v +COQC bedrock2/compiler/src/util/Tactics.v +COQC bedrock2/compiler/src/util/Common.v +COQC Kami/Lib/Indexer.v +COQC bedrock2/compiler/src/util/ListLib.v +COQC Kami/Lib/Misc.v +COQC bedrock2/compiler/src/util/Set.v +COQC Kami/Lib/Word.v +COQC bedrock2/compiler/src/ExprImp.v +End of ExprImp.v +total time: 8.389s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver ---------------------------- 0.0% 49.5% 44 0.222s +─preprocess_impl ----------------------- 0.7% 39.2% 44 0.177s +─abstract_unrecogs --------------------- 16.3% 34.8% 44 0.161s +─set_solver_generic -------------------- 0.2% 15.1% 30 0.405s +─<Coq.Init.Tauto.with_uniform_flags> --- 0.0% 14.9% 34 0.400s +─t_tauto_intuit ------------------------ 3.0% 14.9% 93 0.400s +─remember_unrecogs --------------------- 3.1% 12.3% 548 0.016s +─<Coq.Init.Tauto.simplif> -------------- 9.4% 12.1% 93 0.334s +─map_solver_core ----------------------- 0.5% 10.2% 29 0.085s +─map_solver_core_impl ------------------ 0.3% 9.6% 2 0.084s +─inversion H --------------------------- 9.4% 9.4% 74 0.061s +─inversion_lemma ----------------------- 0.1% 6.2% 9 0.217s +─inversionss --------------------------- 0.1% 6.0% 10 0.226s +─inverts (var) ------------------------- 0.1% 5.9% 63 0.030s +─inverts_tactic ------------------------ 0.2% 5.8% 63 0.030s +─unrecogs_in_prop ---------------------- 5.7% 5.7% 0 0.027s +─map_specialize ------------------------ 0.0% 5.1% 29 0.041s +─map_specialize_step ------------------- 3.7% 5.1% 35 0.036s +─congruence ---------------------------- 4.5% 4.5% 117 0.027s +─invert keep (var) --------------------- 0.1% 4.5% 63 0.028s +─remember P as name eqn:a -------------- 4.5% 4.5% 197 0.012s +─eauto (int_or_var_opt) (int_or_var_opt) 4.3% 4.5% 53 0.055s +─apply mk_Abstracted in a -------------- 3.8% 3.8% 264 0.002s +─replace (uconstr) with (constr) (clause 0.8% 3.6% 21 0.032s +─econstructor -------------------------- 2.8% 2.8% 49 0.010s +─maps_propositional -------------------- 0.1% 2.8% 45 0.043s +─pose proof IH as IH' ------------------ 2.6% 2.6% 3724 0.006s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─map_solver ---------------------------- 0.0% 49.5% 44 0.222s + ├─preprocess_impl --------------------- 0.7% 39.2% 44 0.177s + │└abstract_unrecogs ------------------- 16.3% 34.8% 44 0.161s + │ ├─remember_unrecogs ----------------- 3.1% 12.3% 548 0.016s + │ │ ├─remember P as name eqn:a -------- 4.5% 4.5% 197 0.012s + │ │ └─apply mk_Abstracted in a -------- bedrock2/compiler/src/ExprImp (real: 23.40, user: 10.90, sys: 0.52, mem: 540624 ko) +bedrock2/compiler/src/ZNameGen (real: 1.33, user: 0.46, sys: 0.18, mem: 351756 ko) +bedrock2/compiler/src/examples/TestExprImp (real: 2.02, user: 0.72, sys: 0.26, mem: 458732 ko) +bedrock2/compiler/src/examples/highlevel/FuncMut (real: 1.61, user: 0.55, sys: 0.23, mem: 420416 ko) +File "bedrock2/compiler/src/FlatImp.v", line 418, characters 6-59: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "./Kami/Lib/Word.v", line 2154, characters 0-28: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Lib/Word (real: 55.47, user: 26.60, sys: 0.45, mem: 741048 ko) +File "./Kami/Lib/Struct.v", line 151, characters 0-57: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Lib/Struct (real: 2.57, user: 0.99, sys: 0.21, mem: 435576 ko) +File "bedrock2/compiler/src/FlatImp.v", line 474, characters 6-210: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/FlatImp.v", line 474, characters 6-210: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/FlatImp.v", line 474, characters 6-210: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +Kami/Lib/WordSupport (real: 1.56, user: 0.56, sys: 0.20, mem: 432120 ko) +File "./Kami/Lib/FMap.v", line 563, characters 2-19: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 567, characters 2-51: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 595, characters 2-43: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 618, characters 2-44: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 626, characters 2-41: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 876, characters 2-45: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 913, characters 2-46: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 1328, characters 2-43: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 1475, characters 2-45: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 2482, characters 0-44: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope fmap_scope.". [undeclared-scope,deprecated] +File "./Kami/Lib/FMap.v", line 2681, characters 0-41: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Lib/FMap.v", line 2682, characters 0-48: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Lib/FMap (real: 20.44, user: 9.56, sys: 0.30, mem: 537308 ko) +File "bedrock2/compiler/src/FlatImp.v", line 624, characters 4-95: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "bedrock2/compiler/src/FlatImp.v", line 624, characters 4-95: +Warning: Ltac Profiler cannot yet handle backtracking into multi-success +tactics; profiling results may be wildly inaccurate. +[profile-backtracking,ltac] +File "./Kami/Syntax.v", line 1139, characters 2-33: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Syntax.v", line 1309, characters 0-121: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Syntax.v", line 1315, characters 0-84: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope kami_struct_scope.". [undeclared-scope,deprecated] +File "./Kami/Syntax.v", line 1317, characters 0-54: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope kami_scope.". [undeclared-scope,deprecated] +Kami/Syntax (real: 4.38, user: 1.89, sys: 0.23, mem: 479116 ko) +3.8% 3.8% 264 0.002s + │ └─unrecogs_in_prop ------------------ 5.7% 5.7% 0 0.027s + └─map_solver_core --------------------- 0.5% 10.2% 29 0.085s + └map_solver_core_impl ---------------- 0.3% 9.6% 2 0.084s + ├─map_specialize -------------------- 0.0% 5.1% 29 0.041s + │└map_specialize_step --------------- 3.7% 5.1% 35 0.036s + └─maps_propositional ---------------- 0.1% 2.8% 45 0.043s +─set_solver_generic -------------------- 0.2% 15.1% 30 0.405s +└<Coq.Init.Tauto.with_uniform_flags> --- 0.0% 14.0% 30 0.400s +└t_tauto_intuit ------------------------ 3.0% 14.0% 89 0.400s +└<Coq.Init.Tauto.simplif> -------------- 8.8% 11.3% 89 0.334s +─inversion_lemma ----------------------- 0.1% 6.2% 9 0.217s +└inversionss --------------------------- 0.0% 3.3% 9 0.084s +└inverts (var) ------------------------- 0.0% 3.2% 32 0.020s +└inverts_tactic ------------------------ 0.1% 3.2% 32 0.020s +└invert keep (var) --------------------- 0.0% 2.5% 32 0.018s +─inversion H --------------------------- 6.0% 6.0% 11 0.061s +─replace (uconstr) with (constr) (clause 0.8% 3.6% 21 0.032s +└congruence ---------------------------- 2.8% 2.8% 21 0.027s +─eauto (int_or_var_opt) (int_or_var_opt) 3.2% 3.3% 44 0.023s +─econstructor -------------------------- 2.8% 2.8% 49 0.010s +─inversionss --------------------------- 0.1% 2.7% 1 0.226s +└inverts (var) ------------------------- 0.0% 2.6% 31 0.030s +└inverts_tactic ------------------------ 0.1% 2.6% 31 0.030s +└invert keep (var) --------------------- 0.0% 2.0% 31 0.028s +─pose proof IH as IH' ------------------ 2.6% 2.6% 3724 0.006s + +COQC bedrock2/compiler/src/ZNameGen.v +COQC bedrock2/compiler/src/examples/TestExprImp.v +COQC bedrock2/compiler/src/examples/highlevel/FuncMut.v +COQC bedrock2/compiler/src/FlatImp.v +COQC Kami/Lib/Struct.v +COQC Kami/Lib/WordSupport.v +COQC Kami/Lib/FMap.v +COQC Kami/Syntax.v +COQC Kami/Semantics.v +End of FlatImp.v +total time: 26.926s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─simp ---------------------------------- 0.0% 71.8% 97 2.046s +─simp_step ----------------------------- 0.1% 71.8% 209 0.530s +─unique_inversion ---------------------- 71.4% 71.4% 3388 0.529s +─inversion H --------------------------- 66.5% 66.5% 686 0.199s +─equalities ---------------------------- 0.3% 57.3% 3 10.539s +─map_solver ---------------------------- 0.0% 11.2% 30 0.277s +─preprocess_impl ----------------------- 0.2% 8.1% 30 0.215s +─abstract_unrecogs --------------------- 2.9% 7.0% 30 0.198s +─protect_equalities -------------------- 2.0% 3.8% 593 0.011s +─congruence ---------------------------- 3.6% 3.6% 187 0.043s +─map_solver_core ----------------------- 0.1% 3.1% 25 0.077s +─map_solver_core_impl ------------------ 0.1% 3.0% 2 0.076s +─pose proof IH as IH' ------------------ 2.5% 2.5% 11247 0.004s +─remember_unrecogs --------------------- 0.6% 2.5% 303 0.016s +─inversion_lemma ----------------------- 0.0% 2.3% 11 0.208s +─inversionss --------------------------- 0.0% 2.2% 12 0.246s +─inverts (var) ------------------------- 0.0% 2.2% 81 0.023s +─inverts_tactic ------------------------ 0.1% 2.1% 81 0.023s +─assert (H : e1 = e2) by congruence ---- 0.1% 2.1% 80 0.026s + + tactic bedrock2/compiler/src/FlatImp (real: 62.83, user: 30.21, sys: 0.60, mem: 608088 ko) +bedrock2/compiler/src/util/SetSolverTests (real: 1.00, user: 0.30, sys: 0.15, mem: 290132 ko) +bedrock2/compiler/src/RegAlloc2 (real: 1.61, user: 0.53, sys: 0.21, mem: 386872 ko) +File "./Kami/Semantics.v", line 947, characters 2-35: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Semantics (real: 13.71, user: 6.50, sys: 0.26, mem: 501300 ko) +Kami/Inline (real: 1.93, user: 0.70, sys: 0.23, mem: 469696 ko) +Kami/SymEval (real: 3.58, user: 1.48, sys: 0.24, mem: 476176 ko) +File "./Kami/Wf.v", line 16, characters 2-22: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Wf (real: 6.87, user: 3.06, sys: 0.29, mem: 499932 ko) +File "./Kami/SemFacts.v", line 1666, characters 0-20: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/SemFacts (real: 76.97, user: 37.08, sys: 0.39, mem: 601836 ko) +File "./Kami/ModularFacts.v", line 42, characters 2-30: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/ModularFacts (real: 68.49, user: 32.76, sys: 0.55, mem: 885880 ko) +Kami/StepDet (real: 19.67, user: 9.26, sys: 0.28, mem: 504428 ko) +Kami/Label (real: 7.13, user: 3.17, sys: 0.27, mem: 486656 ko) +Kami/RefinementFacts (real: 18.99, user: 8.98, sys: 0.27, mem: 511956 ko) +Kami/InlineFacts (real: 83.55, user: 40.29, sys: 0.46, mem: 668564 ko) +File "./Kami/Renaming.v", line 16, characters 0-25: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Renaming.v", line 185, characters 2-44: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Renaming.v", line 203, characters 2-58: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Renaming (real: 81.06, user: 39.12, sys: 0.38, mem: 563328 ko) +Kami/Substitute (real: 2.10, user: 0.72, sys: 0.26, mem: 473852 ko) +Kami/Decomposition (real: 11.95, user: 5.56, sys: 0.26, mem: 507520 ko) +Kami/Amortization (real: 11.22, user: 5.12, sys: 0.29, mem: 505436 ko) +Kami/SymEvalTac (real: 1.93, user: 0.67, sys: 0.23, mem: 474056 ko) +Kami/PartialInlineFacts (real: 13.41, user: 6.24, sys: 0.29, mem: 509232 ko) +Kami/ParametricSyntax (real: 31.00, user: 14.78, sys: 0.34, mem: 561068 ko) +File "./Kami/Specialize.v", line 858, characters 2-44: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Specialize.v", line 1194, characters 0-130: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Specialize (real: 45.09, user: 21.68, sys: 0.30, mem: 506640 ko) +Kami/ParametricWf (real: 5.32, user: 2.19, sys: 0.29, mem: 489072 ko) +File "./Kami/ParametricEquiv.v", line 10, characters 2-22: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/ParametricEquiv (real: 6.90, user: 3.10, sys: 0.28, mem: 492424 ko) +File "./Kami/Notations.v", line 28, characters 0-81: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope kami_expr_scope.". [undeclared-scope,deprecated] +File "./Kami/Notations.v", line 89, characters 0-169: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope init_scope.". [undeclared-scope,deprecated] +File "./Kami/Notations.v", line 110, characters 0-190: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope kami_action_scope.". [undeclared-scope,deprecated] +File "./Kami/Notations.v", line 263, characters 0-212: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope kami_sin_scope.". [undeclared-scope,deprecated] +File "./Kami/Notations.v", line 404, characters 0-247: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope kami_gen_scope.". [undeclared-scope,deprecated] +File "./Kami/Notations.v", line 663, characters 0-260: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope kami_meta_scope.". [undeclared-scope,deprecated] +Kami/Notations (real: 2.42, user: 0.87, sys: 0.28, mem: 460284 ko) +Kami/Duplicate (real: 5.46, user: 2.39, sys: 0.28, mem: 487424 ko) +Kami/Synthesize (real: 1.72, user: 0.59, sys: 0.24, mem: 442252 ko) +Kami/Ex/MemTypes (real: 1.99, user: 0.71, sys: 0.23, mem: 452980 ko) +Kami/Ext/BSyntax (real: 2.19, user: 0.79, sys: 0.27, mem: 477872 ko) +Kami/ParametricInline (real: 9.22, user: 4.19, sys: 0.30, mem: 509168 ko) +Kami/ModuleBound (real: 3.21, user: 1.29, sys: 0.27, mem: 485936 ko) +File "./Kami/ModuleBoundEx.v", line 25, characters 2-71: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope namebound_scope.". [undeclared-scope,deprecated] +File "./Kami/ModuleBoundEx.v", line 332, characters 2-71: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope namebound_scope.". [undeclared-scope,deprecated] +Kami/ModuleBoundEx (real: 7.16, user: 3.17, sys: 0.30, mem: 492768 ko) +Kami/ParamDup (real: 5.47, user: 2.42, sys: 0.25, mem: 489812 ko) +File "./Kami/Tactics.v", line 923, characters 0-59: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Tactics.v", line 924, characters 0-77: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Tactics.v", line 984, characters 0-543: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope mapping_scope.". [undeclared-scope,deprecated] +Kami/Tactics (real: 2.58, user: 0.89, sys: 0.26, mem: 484828 ko) +Kami/ParametricInlineLtac (real: 2.11, user: 0.77, sys: 0.26, mem: 486708 ko) +Kami/MapReifyEx (real: 4.56, user: 1.94, sys: 0.29, mem: 494008 ko) +File "./Kami/Ex/SC.v", line 432, characters 2-30: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/SC.v", line 441, characters 2-33: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/SC.v", line 460, characters 0-72: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/SC (real: 8.37, user: 3.81, sys: 0.27, mem: 510132 ko) +File "./Kami/Ex/OneEltFifo.v", line 85, characters 0-50: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/OneEltFifo.v", line 86, characters 0-56: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/OneEltFifo.v", line 87, characters 0-56: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/OneEltFifo (real: 2.92, user: 1.15, sys: 0.26, mem: 487776 ko) +File "./Kami/Ex/Fifo.v", line 197, characters 2-29: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/Fifo.v", line 202, characters 2-35: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/Fifo.v", line 207, characters 2-30: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/Fifo.v", line 212, characters 2-36: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/Fifo.v", line 266, characters 0-167: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/Fifo.v", line 270, characters 0-175: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/Fifo (real: 16.06, user: 7.55, sys: 0.28, mem: 534616 ko) +File "./Kami/Ex/NativeFifo.v", line 174, characters 2-35: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/NativeFifo.v", line 181, characters 2-41: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/NativeFifo.v", line 188, characters 2-36: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/NativeFifo.v", line 195, characters 2-42: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/NativeFifo.v", line 273, characters 0-215: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/NativeFifo.v", line 277, characters 0-223: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/NativeFifo (real: 4.03, user: 1.70, sys: 0.27, mem: 490720 ko) +File "./Kami/Ex/IsaRv32.v", line 88, characters 0-79: +Warning: Notation "$ _" was already used in scope kami_expr_scope. +[notation-overridden,parsing] +Kami/Ex/IsaRv32 (real: 3.31, user: 1.30, sys: 0.26, mem: 509008 ko) +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +ndiXq cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +HndiXq cannot be defined because the projection ndiXq was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +ndiX cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: HndiX cannot be defined because the projection ndiX was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +ndiD cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: HndiD cannot be defined because the projection ndiD was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +ndiDp cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +HndiDp cannot be defined because the projection ndiDp was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +ndiDn cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +HndiDn cannot be defined because the projection ndiDn was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +ndiCnt cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +HndiCnt cannot be defined because the projection ndiCnt was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +HndiDdp cannot be defined because the projections ndiDp, ndiD were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +HndiDdn cannot be defined because the projections ndiDn, ndiDp were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Divider32.v", line 1058, characters 2-1168: +Warning: +HndiInv cannot be defined because the projections ndiD, ndiCnt, ndiXq, ndiX, +ndiD were not defined. [cannot-define-projection,records] +Kami/Ex/Divider32 (real: 125.49, user: 60.73, sys: 0.58, mem: 847228 ko) +File "./Kami/Ex/Multiplier64.v", line 399, characters 2-24: +Warning: Use of “Require” inside a section is deprecated. +[require-in-section,deprecated] +File "./Kami/Ex/Multiplier64.v", line 431, characters 4-143: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bword_scope.". [undeclared-scope,deprecated] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +bsiM cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: HbsiM cannot be defined because the projection bsiM was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +bsiR cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: HbsiR cannot be defined because the projection bsiR was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +bsiMp cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +HbsiMp cannot be defined because the projection bsiMp was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +bsiMn cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +HbsiMn cannot be defined because the projection bsiMn was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +bsiP cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: HbsiP cannot be defined because the projection bsiP was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +bsiCnt cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +HbsiCnt cannot be defined because the projection bsiCnt was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +HbsiMmp cannot be defined because the projections bsiMp, bsiM were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +HbsiMmn cannot be defined because the projections bsiMn, bsiM were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: HmInv cannot be defined because the projection bsiM was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier64.v", line 1125, characters 2-1192: +Warning: +HbsiInv cannot be defined because the projections bsiCnt, bsiP, bsiM, bsiR +were not defined. [cannot-define-projection,records] +Kami/Ex/Multiplier64 (real: 430.88, user: 206.96, sys: 1.70, mem: 1980772 ko) +File "./Kami/Ex/Multiplier32.v", line 399, characters 2-24: +Warning: Use of “Require” inside a section is deprecated. +[require-in-section,deprecated] +File "./Kami/Ex/Multiplier32.v", line 431, characters 4-143: +Warning: Declaring a scope implicitly is deprecated; use in advance an +explicit "Declare Scope bword_scope.". [undeclared-scope,deprecated] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +bsiM cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: HbsiM cannot be defined because the projection bsiM was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +bsiR cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: HbsiR cannot be defined because the projection bsiR was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +bsiMp cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +HbsiMp cannot be defined because the projection bsiMp was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +bsiMn cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +HbsiMn cannot be defined because the projection bsiMn was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +bsiP cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: HbsiP cannot be defined because the projection bsiP was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +bsiCnt cannot be defined because it is informative and BoothMultiplierInv is +not. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +HbsiCnt cannot be defined because the projection bsiCnt was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +HbsiMmp cannot be defined because the projections bsiMp, bsiM were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +HbsiMmn cannot be defined because the projections bsiMn, bsiM were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: HmInv cannot be defined because the projection bsiM was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Multiplier32.v", line 1125, characters 2-1192: +Warning: +HbsiInv cannot be defined because the projections bsiCnt, bsiP, bsiM, bsiR +were not defined. [cannot-define-projection,records] + local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─equalities ---------------------------- 0.3% 57.3% 3 10.539s + ├─simp -------------------------------- 0.0% 54.9% 77 2.046s + │└simp_step --------------------------- 0.0% 54.9% 160 0.530s + │└unique_inversion -------------------- 54.6% 54.6% 2632 0.529s + │ ├─inversion H ----------------------- 47.8% 47.8% 454 0.170s + │ └─protect_equalities ---------------- 1.7% 3.3% 454 0.010s + └─assert (H : e1 = e2) by congruence -- 0.1% 2.1% 80 0.026s + └congruence -------------------------- 2.0% 2.0% 80 0.025s +─simp ---------------------------------- 0.0% 17.0% 20 0.417s +└simp_step ----------------------------- 0.0% 17.0% 49 0.396s +└unique_inversion ---------------------- 16.8% 16.8% 756 0.395s +└inversion H --------------------------- 15.4% 15.4% 139 0.199s +─map_solver ---------------------------- 0.0% 11.2% 30 0.277s + ├─preprocess_impl --------------------- 0.2% 8.1% 30 0.215s + │└abstract_unrecogs ------------------- 2.9% 7.0% 30 0.198s + │└remember_unrecogs ------------------- 0.6% 2.5% 303 0.016s + └─map_solver_core --------------------- 0.1% 3.1% 25 0.077s + └map_solver_core_impl ---------------- 0.1% 3.0% 2 0.076s +─pose proof IH as IH' ------------------ 2.5% 2.5% 11247 0.004s +─inversion_lemma ----------------------- 0.0% 2.3% 11 0.208s + +COQC bedrock2/compiler/src/util/SetSolverTests.v +COQC bedrock2/compiler/src/RegAlloc2.v +COQC bedrock2/compiler/src/FlattenExpr.v +COQC Kami/Inline.v +COQC Kami/SymEval.v +COQC Kami/Wf.v +COQC Kami/SemFacts.v +COQC Kami/ModularFacts.v +COQC Kami/StepDet.v +COQC Kami/Label.v +COQC Kami/RefinementFacts.v +COQC Kami/InlineFacts.v +COQC Kami/Renaming.v +COQC Kami/Substitute.v +COQC Kami/Decomposition.v +COQC Kami/Amortization.v +COQC Kami/SymEvalTac.v +COQC Kami/PartialInlineFacts.v +COQC Kami/ParametricSyntax.v +COQC Kami/Specialize.v +COQC Kami/ParametricWf.v +COQC Kami/ParametricEquiv.v +COQC Kami/Notations.v +COQC Kami/Duplicate.v +COQC Kami/Synthesize.v +COQC Kami/Ex/MemTypes.v +COQC Kami/Ext/BSyntax.v +COQC Kami/ParametricInline.v +COQC Kami/ModuleBound.v +COQC Kami/ModuleBoundEx.v +COQC Kami/ParamDup.v +COQC Kami/Tactics.v +COQC Kami/ParametricInlineLtac.v +COQC Kami/MapReifyEx.v +COQC Kami/Ex/SC.v +COQC Kami/Ex/OneEltFifo.v +COQC Kami/Ex/Fifo.v +COQC Kami/Ex/NativeFifo.v +COQC Kami/Ex/IsaRv32.v +COQC Kami/Ex/Divider32.v +COQC Kami/Ex/Multiplier64.v +COQC Kami/Ex/Multiplier32.v +End of FlattenExpr.v +total time: 587.422s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─maps ---------------------------------- 0.0% 88.3% 84 17.968s +─map_solver ---------------------------- 0.0% 54.8% 95 9.899s +─map_solver_core ----------------------- 0.1% 42.7% 92 9.552s +─map_solver_core_impl ------------------ 0.0% 42.6% 13 9.549s +─default_flattenBooleanExpr ------------ 0.0% 37.3% 21 36.430s +─map_specialize ------------------------ 0.0% 36.3% 92 7.801s +─map_specialize_step ------------------- 24.9% 36.3% 1911 5.056s +─pose_flatten_var_ineqs ---------------- 4.0% 34.0% 86 10.352s +─unique eapply (constr) in copy of (iden 1.0% 30.1% 59814 0.049s +─unshelve (tactic1) -------------------- 0.7% 26.8% 59814 0.048s +─eapply p in H' ------------------------ 26.2% 26.2% 59814 0.048s +─preprocess_impl ----------------------- 0.0% 12.1% 95 2.152s +─abstract_unrecogs --------------------- 7.0% 11.1% 95 2.057s +─simp ---------------------------------- 0.0% 6.3% 78 3.196s +─simp_step ----------------------------- 0.0% 6.3% 644 1.145s +─maps_propositional -------------------- 0.0% 6.0% 480 7.295s +─unique_inversion ---------------------- 3.9% 3.9% 5338 1.144s +─maps_leaf_tac ------------------------- 0.1% 3.5% 2100 0.035s +─inversion H --------------------------- 3.4% 3.4% 1097 1.070s +─congruence ---------------------------- 3.2% 3.2% 2495 0.085s +─pose proof H as H' -------------------- 3.1% 3.1% 185783 0.026s +─canonicalize_map_hyp ------------------ 0.6% 2.9% 37401 0.022s +─specialize (constr_with_bindings) ----- 2.5% 2.5% 166250 0.022s +─destruct_unique_match ----------------- 2.4% 2.4% 821 0.389s +─remember_unrecogs --------------------- 0.9% 2.4% 2727 0.644s +─ensure_no_body ------------------------ 1.0% 2.3% 161949 0.015s +─propositional_cheap_step -------------- 2.2% 2.3% 3800 0.016s +─auto (int_or_var_opt) (auto_using) (hin 1.8% 2.1% 3290 0.023s +─assert_fails -------------------------- 0.6% 2.0% 196767 0.023s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─maps ---------------------------------- 0.0% 52.5% 53 17.968s + ├─map_solver -------------------------- 0.0% 30.3% 64 9.899s + │ ├─map_solver_core ------------------- 0.0% 22.4% 64 9.552s + │ │└map_solver_core_impl -------------- 0.0% 22.4% 1 9.549s + │ │ ├─map_specialize ------------------ 0.0% 17.8% 64 5.088s + │ │ │└map_specialize_step ------------- 12.7% 17.8% 1057 4.472s + │ │ └─maps_propositional -------------- 0.0% 4.4% 350 7.295s + │ │ └maps_leaf_tac ------------------- 0.0% 2.5% 1634 0.025s + │ └─preprocess_impl ------------------- 0.0% 7.9% 64 2.152s + │ └abstract_unrecogs ----------------- 4.6% 7.3% 64 2.057s + └─pose_flatten_var_ineqs -------------- 2.5% 22.1% 53 10.352s + └unique eapply (constr) in copy of (id 0.6% 19.7% 36953 0.049s + └unshelve (tactic1) ------------------ 0.4% 17.8% 36953 0.048s + └eapply p in H' ---------------------- 17.4% 17.4% 36953 0.048s +─default_flattenBooleanExpr ------------ 0.0% 37.3% 21 36.430s + ├─maps -------------------------------- 0.0% 35.0% 30 12.207s + │ ├─map_solver ------------------------ 0.0% 24.0% 30 9.184s + │ │ ├─map_solver_core ----------------- 0.0% 20.1% 27 7.870s + │ │ │└map_solver_core_impl ------------ 0.0% 20.1% 12 7.859s + │ │ │└map_specialize ------------------ 0.0% 18.3% 27 7.801s + │ │ │└map_specialize_step ------------- 12.1% 18.3% 845 5.056s + │ │ └─preprocess_impl ----------------- 0.0% 3.9% 30 1.349s + │ │ └abstract_unrecogs --------------- 2.3% 3.6% 30 1.238s + │ └─pose_flatten_var_ineqs ------------ 1.4% 11.0% 30 3.250s + │ └unique eapply (constr) in copy of ( 0.4% 9.6% 21011 0.027s + │ └unshelve (tactic1) ---------------- 0.2% 8.3% 21011 0.027s + │ └eapply p in H' -------------------- 8.1% 8.1% 21011 0.027s + └─simp -------------------------------- 0.0% 2.2% 21 1.839s + └simp_step --------------------------- 0.0% 2.1% 243 0.174s +─simp ---------------------------------- 0.0% 4.2% 57 3.196s +└simp_step ----------------------------- 0.0% 4.2% 401 1.145s +└unique_inversion --------bedrock2/compiler/src/FlattenExpr (real: 1225.77, user: 593.01, sys: 9.58, mem: 1060368 ko) +bedrock2/compiler/src/examples/TestFlatImp (real: 4.39, user: 0.71, sys: 0.28, mem: 459820 ko) +bedrock2/compiler/src/FlatToRiscvDef (real: 2.44, user: 0.69, sys: 0.24, mem: 466532 ko) +bedrock2/compiler/src/RegAlloc3 (real: 1.44, user: 0.50, sys: 0.18, mem: 389304 ko) +bedrock2/compiler/src/EmitsValid (real: 49.36, user: 23.66, sys: 0.35, mem: 610544 ko) +bedrock2/compiler/src/RegAllocAnnotatedNotations (real: 1.73, user: 0.45, sys: 0.18, mem: 350576 ko) +bedrock2/compiler/src/GoFlatToRiscv (real: 15.43, user: 6.89, sys: 0.27, mem: 480324 ko) +bedrock2/compiler/src/FlatToRiscv32 (real: 17.62, user: 8.26, sys: 0.29, mem: 505664 ko) +Kami/Ex/Multiplier32 (real: 214.00, user: 104.11, sys: 0.86, mem: 1131272 ko) +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +ndiXq cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +HndiXq cannot be defined because the projection ndiXq was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +ndiX cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: HndiX cannot be defined because the projection ndiX was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +ndiD cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: HndiD cannot be defined because the projection ndiD was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +ndiDp cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +HndiDp cannot be defined because the projection ndiDp was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +ndiDn cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +HndiDn cannot be defined because the projection ndiDn was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +ndiCnt cannot be defined because it is informative and NrDividerInv is not. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +HndiCnt cannot be defined because the projection ndiCnt was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +HndiDdp cannot be defined because the projections ndiDp, ndiD were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +HndiDdn cannot be defined because the projections ndiDn, ndiDp were not +defined. [cannot-define-projection,records] +File "./Kami/Ex/Divider64.v", line 1058, characters 2-1168: +Warning: +HndiInv cannot be defined because the projections ndiD, ndiCnt, ndiXq, ndiX, +ndiD were not defined. [cannot-define-projection,records] +Kami/Ex/Divider64 (real: 271.33, user: 131.59, sys: 1.01, mem: 1411224 ko) +bedrock2/compiler/src/FlatToRiscv (real: 415.73, user: 202.44, sys: 0.75, mem: 899104 ko) +bedrock2/compiler/src/Pipeline (real: 5.85, user: 2.50, sys: 0.27, mem: 505076 ko) +Kami/Ex/FifoCorrect (real: 125.57, user: 61.07, sys: 0.56, mem: 798376 ko) +File "./Kami/Ex/RegFile.v", line 132, characters 0-66: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/RegFile.v", line 133, characters 0-69: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/RegFile (real: 4.25, user: 1.81, sys: 0.24, mem: 495792 ko) +Kami/Ex/SCMMInl (real: 11.10, user: 5.07, sys: 0.30, mem: 561800 ko) +Kami/Kami (real: 2.25, user: 0.74, sys: 0.24, mem: 485920 ko) +File "./Kami/Ex/MemAtomic.v", line 121, characters 2-29: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +bedrock2/compiler/src/examples/MMIO (real: 32.79, user: 15.63, sys: 0.31, mem: 555732 ko) +File "./Kami/Ex/MemAtomic.v", line 128, characters 2-28: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/MemAtomic.v", line 137, characters 2-29: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/MemAtomic.v", line 144, characters 2-29: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/MemAtomic.v", line 166, characters 0-146: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/MemAtomic (real: 3.50, user: 1.47, sys: 0.24, mem: 497260 ko) +bedrock2/compiler/src/examples/InlineAssemblyMacro (real: 1.97, user: 0.71, sys: 0.26, mem: 483356 ko) +bedrock2/compiler/src/examples/CompileExamples (real: 2.52, user: 0.74, sys: 0.21, mem: 501084 ko) +bedrock2/compiler/src/examples/Fibonacci (real: 7.21, user: 3.30, sys: 0.23, mem: 510956 ko) +-------------- 3.2% 3.2% 3570 1.144s +└inversion H --------------------------- 2.7% 2.7% 626 1.070s + +COQC bedrock2/compiler/src/examples/TestFlatImp.v +COQC bedrock2/compiler/src/FlatToRiscvDef.v +COQC bedrock2/compiler/src/RegAlloc3.v +COQC bedrock2/compiler/src/EmitsValid.v +COQC bedrock2/compiler/src/RegAllocAnnotatedNotations.v +COQC bedrock2/compiler/src/GoFlatToRiscv.v +COQC bedrock2/compiler/src/FlatToRiscv32.v +COQC bedrock2/compiler/src/FlatToRiscv.v +COQC Kami/Ex/Divider64.v +COQC Kami/Ex/FifoCorrect.v +COQC bedrock2/compiler/src/Pipeline.v +COQC bedrock2/compiler/src/examples/MMIO.v +compiled@{} = +[[Lui addr 268582912; Addi addr addr 0; Lw i addr 0; +Beq i 0 16; Mul s i i; Sw addr s 0; Jal 0 (-16)]] + : list Instruction +COQC Kami/Ex/RegFile.v +COQC Kami/Ex/SCMMInl.v +COQC Kami/Kami.v +COQC Kami/Ex/MemAtomic.v +COQC bedrock2/compiler/src/examples/InlineAssemblyMacro.v +COQC Kami/Ex/SimpleFifoCorrect.v +compiled@{} = +[[Lw 9 1 0; Mul 4 2 3; Add 5 2 3; Sub 6 2 3; Auipc 31 0; +Add 31 31 9; Jalr 0 31 8; Addi 7 4 0; Jal 0 20; Addi 7 5 0; +Jal 0 12; Addi 7 6 0; Jal 0 4]] + : list Instruction +COQC bedrock2/compiler/src/examples/CompileExamples.v +COQC bedrock2/compiler/src/examples/Fibonacci.v +fib_ExprImp@{compiler.examples.Fibonacci.17} = +fun n : Z => +cmd.seq (cmd.set 1 (expr.literal 0)) + (cmd.seq (cmd.set 2 (expr.literal 1)) + (cmd.seq (cmd.set 4 (expr.literal 0)) + (cmd.while (expr.op ltu (expr.var 4) (expr.literal n)) + (cmd.seq (cmd.set 3 (expr.op add (expr.var 1) (expr.var 2))) + (cmd.seq (cmd.set 1 (expr.var 2)) + (cmd.seq (cmd.set 2 (expr.var 3)) + (cmd.set 4 (expr.op add (expr.var 4) (expr.literal 1))))))))) + : Z -> cmd + +Argument scope is [Z_scope] + = SSeq (SLit 1 0) + (SSeq (SLit 2 1) + (SSeq (SLit 4 0) + (SLoop (SSeq SSkip (SLit 5 6)) (CondBinary BLtu 4 5) + (SSeq (SSeq SSkip (SSeq SSkip (SOp 3 add 1 2))) + (SSeq (SSet 1 2) + (SSeq (SSet 2 3) + (SSeq SSkip (SSeq (SLit 6 1) (SOp 4 add 4 6))))))))) + : stmt +Finished transaction in 0.012 secs (0.007u,0.s) (successful) +fib6_riscv@{} = +[Addi 1 0 0; Addi 2 0 1; Addi 4 0 0; Addi 5 0 6; Bgeu 4 5 28; +Add 3 1 2; Add 1 0 2; Add 2 0 3; Addi 6 0 1; Add 4 4 6; +Jal 0 (-28)] + : list Instruction +fib6_riscv@{} = +RISCV: + addi x1, x0, 0 + addi x2, x0, 1 + addi x4, x0, 0 + addi x5, x0, 6 + bgeu x4, x5, 28 + add x3, x1, x2 + add x1, x0, x2 + add x2, x0, x3 + addi x6, x0, 1 + add x4, x4, x6 + jal x0, -28 + : list Instruction +93000000 13011000 13020000 93026000 637e5200 b3812000 b3002000 33013000 +13031000 33026200 6ff05ffe + = {| Naive.unsigned := 13; Naive._unsigned_in_range := eq_refl |} + : word +COQC bedrock2/compiler/src/examples/FE310Compiler.v +Finished transaction in 0.063 secs (0.028u,0.001s) (successful) +Axioms: +AdmitAxiom.proof_admitted : False + used in map_ok_subproof5 to prove: forall (m1 m2 : map p ok) + (k : parameters.key) + (v : parameters.value), + map.get m2 k = Some v -> + map.get (map.putmany m1 m2) k = Some v + used in map_ok_subproof4 to prove: forall (m1 m2 : map p ok) + (k : parameters.key), + map.get m2 k = None -> + map.get (map.putmany m1 m2) k = + map.get m1 k + used in map_ok_subproof3 to prove: forall (m : map p ok) + (k k' : parameters.key), + k <> k' -> + map.get (map.remove m k') k = map.get m k + used in map_ok_subproof2 to prove: forall (m : map p ok) + (k : parameters.key), + map.get (map.remove m k) k = None + used in map_ok_subproof1 to prove: forall (m : map p ok) + (k : parameters.key) + (v : parameters.value) + (k' : parameters.key), + k <> k' -> + map.get (map.put m k' v) k = map.get m k + used in map_ok_subproof0 to prove: forall (m : map p ok) + (k : parameters.key) + (v : parameters.value), + map.get (map.put m k v) k = Some v + used in map_ok_subproof to prove: forall m1 m2 : map p ok, + (forall k : parameters.key, + map.get m1 k = map.get m2 k) -> + m1 = m2 +ext_spec_Proper : forall + (trace : list + (mem * actname * list Semantics.word * + (mem * list Semantics.word))) + (m : mem) (act : actname) (args : list Semantics.word), + Morphisms.Proper + (Morphisms.respectful + (Morphisms.pointwise_relation mem + (Morphisms.pointwise_relation + (list Semantics.word) Basics.impl)) Basics.impl) + (ext_spec trace m act args) +Axioms: +FlatToRiscv.word_eq_dec : forall p : FlatToRiscv.FlatToRiscv.parameters, + FlatToRiscv.FlatToRiscv.assumptions -> + DecidableEq word +undef_on_unchecked_store_byte_tuple_list : forall + (n : nat) + (l : list (HList.tuple word8 n)) + (start : word32), + map.undef_on + (unchecked_store_byte_tuple_list + start l map.empty) + (fun x : word32 => + ~ + word.unsigned start <= + word.unsigned x < + word.unsigned start + + Z.of_nat n * Zlength l) +store_program_empty : forall (prog : list Instruction) (addr : word), + GoFlatToRiscv.program addr prog + (unchecked_store_program addr prog map.empty) +FlatToRiscv.reduce_eq_to_sub_and_lt : forall + p : FlatToRiscv.FlatToRiscv.parameters, + FlatToRiscv.FlatToRiscv.assumptions -> + forall (y z : word) + (T : Type) + (thenVal elseVal : T), + (if word.eqb y z + then thenVal + else elseVal) = + (if + word.ltu (word.sub y z) (word.of_Z 1) + then thenVal + else elseVal) +real_ext_spec_implies_simple_ext_spec : forall (p : MMIO.parameters) + (t : trace) + (m : MMIO.mem) + (a : MMIOAction) + (args : list MMIO.word) + (post : + MMIO.mem -> + list MMIO.word -> Prop), + real_ext_spec t m a args post -> + simple_ext_spec t m a args post +FlatToRiscv.put_put_same : forall (K V : Type) (M : map.map K V) + (k : K) (v1 v2 : V) (m : M), + map.put (map.put m k v1) k v2 = map.put m k v2 +PropExtensionality.propositional_extensionality : +forall P Q : Prop, P <-> Q -> P = Q +AdmitAxiom.proof_admitted : False + used in map_ok_subproof5 to prove: forall (m1 m2 : map p ok) + (k : parameters.key) + (v : parameters.value), + map.get m2 k = Some v -> + map.get (map.putmany m1 m2) k = Some v + used in map_ok_subproof4 to prove: forall (m1 m2 : map p ok) + (k : parameters.key), + map.get m2 k = None -> + map.get (map.putmany m1 m2) k = + map.get m1 k + used in map_ok_subproof3 to prove: forall (m : map p ok) + (k k' : parameters.key), + k <> k' -> + map.get (map.remove m k') k = map.get m k + used in map_ok_subproof2 to prove: forall (m : map p ok) + (k : parameters.key), + map.get (map.remove m k) k = None + used in map_ok_subproof1 to prove: forall (m : map p ok) + (k : parameters.key) + (v : parameters.value) + (k' : parameters.key), + k <> k' -> + map.get (map.put m k' v) k = map.get m k + used in map_ok_subproof0 to prove: forall (m : map p ok) + (k : parameters.key) + (v : parameters.value), + map.get (map.put m k v) k = Some v + used in map_ok_subproof to prove: forall m1 m2 : map p ok, + (forall k : parameters.key, + map.get m1 k = map.get m2 k) -> + m1 = m2 +max_ext_call_code_size_bound : forall (p : FlattenExpr.parameters) + (f : FlattenExpr.actname), + 0 <= FlattenExpr.max_ext_call_code_size f <= 7 +map_undef_on_weaken : forall (P Q : PropSet.set word32) (m : Mem), + map.undef_on m Q -> + PropSet.subset P Q -> map.undef_on m P +FlatImp.exec.map_split_diff : forall pp : Semantics.parameters, + FlatImp.env -> + forall m m1 m2 m3 : mem, + map.split m m2 m1 -> + map.split m m3 m1 -> m2 = m3 +load4bytes_in_MMIO_is_None : forall (p : MMIO.parameters) + (m : MMIO.mem) (addr : MMIO.word), + map.undef_on m isMMIOAddr -> + isMMIOAddr addr -> load_bytes 4 m addr = None +FunctionalExtensionality.functional_extensionality_dep : +forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), +(forall x : A, f x = g x) -> f = g +FlatImp.exec.ext_spec_intersect : forall (pp : Semantics.parameters) + (t : list + (mem * actname * + list Semantics.word * + (mem * list Semantics.word))) + (mGive1 mGive2 : mem) + (a : actname) + (args : list Semantics.word) + (post1 + post2 : mem -> + list Semantics.word -> Prop), + ext_spec t mGive1 a args post1 -> + ext_spec t mGive2 a args post2 -> + mGive1 = mGive2 /\ + ext_spec t mGive1 a args + (fun (mReceive : mem) + (resvals : list Semantics.word) => + post1 mReceive resvals /\ + post2 mReceive resvals) +ext_spec_Proper : forall + (trace : list + (mem * actname * list Semantics.word * + (mem * list Semantics.word))) + (m : mem) (act : actname) (args : list Semantics.word), + Morphisms.Proper + (Morphisms.respectful + (Morphisms.pointwise_relation mem + (Morphisms.pointwise_relation + (list Semantics.word) Basics.impl)) Basics.impl) + (ext_spec trace m act args) +FlatToRiscv.divisibleBy4_admit : forall + p : FlatToRiscv.FlatToRiscv.parameters, + FlatToRiscv.FlatToRiscv.assumptions -> + forall x y : word, + FlatToRiscv.divisibleBy4 x -> + FlatToRiscv.divisibleBy4 y +compile_lit_new_size : forall iset : InstructionSet, + FlatToRiscvDef.FlatToRiscvDef.parameters -> + forall (x : Register) (v : Z), + 0 <= + Zlength (FlatToRiscvDef.compile_lit_new iset x v) <= + 15 +FlatToRiscv.compile_lit_correct_full : forall + p : FlatToRiscv.FlatToRiscv.parameters, + FlatToRiscv.FlatToRiscv.assumptions -> + forall + (initialL : + RiscvMachine.RiscvMachine + Syntax.varname + FlatToRiscvDef.FlatToRiscvDef.actname) + (post : RiscvMachine.RiscvMachine + Register + FlatToRiscvDef.FlatToRiscvDef.actname -> + Prop) + (x : Syntax.varname) + (v : Z) + (R : FlatToRiscv.FlatToRiscv.mem -> + Prop), + getNextPc initialL = + add (getPc initialL) (ZToReg 4) -> + let insts := + FlatToRiscvDef.compile_stmt + FlatToRiscv.FlatToRiscv.iset + (FlatImp.SLit x v) in + let d := + mul (ZToReg 4) + (ZToReg (Zlength insts)) in + Separation.sep + (GoFlatToRiscv.program + (getPc initialL) insts) R + (getMem initialL) -> + FlatToRiscvDef.valid_registers + (FlatImp.SLit x v) -> + FlatToRiscv.runsTo + (withRegs + (map.put + (getRegs inibedrock2/compiler/src/examples/FE310Compiler (real: 42.80, user: 20.27, sys: 0.35, mem: 610324 ko) +bedrock2/compiler/src/examples/EditDistExample (real: 2.19, user: 0.80, sys: 0.26, mem: 499980 ko) +bedrock2/compiler/src/examples/swap_bytes_over_uart_hexdump (real: 2.04, user: 0.74, sys: 0.23, mem: 505316 ko) +Kami/Ex/IsaRv32Pgm (real: 2.28, user: 0.82, sys: 0.26, mem: 507796 ko) +File "./Kami/Ex/ProcDec.v", line 279, characters 2-29: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcDec.v", line 289, characters 2-30: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcDec.v", line 301, characters 2-31: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcDec.v", line 314, characters 0-76: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/ProcDec (real: 9.01, user: 4.13, sys: 0.26, mem: 512264 ko) +Kami/Ext/Extraction (real: 2.36, user: 0.79, sys: 0.24, mem: 488532 ko) +Kami/Ex/SimpleFifoCorrect (real: 74.95, user: 37.44, sys: 0.37, mem: 672092 ko) +File "./Kami/Tutorial.v", line 72, characters 0-27: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 801, characters 2-32: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Tutorial (real: 7.47, user: 3.39, sys: 0.25, mem: 517872 ko) +File "./Kami/Ex/ProcThreeStage.v", line 806, characters 2-35: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 811, characters 2-35: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 816, characters 2-38: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 821, characters 2-38: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 831, characters 2-36: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 839, characters 2-33: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 844, characters 2-30: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/IsaRv32/PgmGcd (real: 4.45, user: 1.88, sys: 0.27, mem: 521816 ko) +File "./Kami/Ex/ProcThreeStage.v", line 855, characters 2-27: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStage.v", line 871, characters 0-251: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/ProcThreeStage (real: 12.09, user: 5.62, sys: 0.28, mem: 535096 ko) +Kami/Ex/IsaRv32/PgmFact (real: 4.26, user: 1.83, sys: 0.25, mem: 522312 ko) +Kami/Ex/IsaRv32/PgmBsort (real: 4.09, user: 1.75, sys: 0.23, mem: 521896 ko) +Kami/Ex/IsaRv32/PgmHanoi (real: 4.05, user: 1.74, sys: 0.23, mem: 522080 ko) +Kami/Ex/IsaRv32/PgmDekker1 (real: 4.24, user: 1.78, sys: 0.27, mem: 520604 ko) +Kami/Ex/IsaRv32/PgmDekker2 (real: 4.29, user: 1.83, sys: 0.25, mem: 524584 ko) +Kami/Ex/IsaRv32/PgmPeterson1 (real: 4.23, user: 1.80, sys: 0.27, mem: 519680 ko) +Kami/Ex/IsaRv32/PgmPeterson2 (real: 4.14, user: 1.80, sys: 0.24, mem: 519696 ko) +Kami/Ex/IsaRv32/PgmMatMulInit (real: 4.29, user: 1.81, sys: 0.25, mem: 521416 ko) +Kami/Ex/IsaRv32/PgmMatMulNormal1 (real: 4.30, user: 1.83, sys: 0.26, mem: 519240 ko) +Kami/Ex/IsaRv32/PgmMatMulNormal2 (real: 4.21, user: 1.81, sys: 0.24, mem: 519724 ko) +Kami/Ex/IsaRv32/PgmMatMulReport (real: 4.32, user: 1.87, sys: 0.25, mem: 519908 ko) +Kami/Ex/IsaRv32/PgmBankerInit (real: 4.21, user: 1.81, sys: 0.24, mem: 522124 ko) +Kami/Ex/IsaRv32/PgmBankerWorker1 (real: 4.43, user: 1.87, sys: 0.27, mem: 522776 ko) +Kami/Ex/IsaRv32/PgmBankerWorker2 (real: 4.24, user: 1.80, sys: 0.25, mem: 520460 ko) +Kami/Ex/ProcThreeStInl (real: 2.03, user: 0.75, sys: 0.23, mem: 490144 ko) +Kami/Ex/IsaRv32/PgmBankerWorker3 (real: 4.25, user: 1.85, sys: 0.24, mem: 520188 ko) +File "./Kami/Ex/ProcFetchDecode.v", line 333, characters 2-32: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcFetchDecode.v", line 342, characters 2-32: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcFetchDecode.v", line 356, characters 0-68: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/ProcFetchDecode (real: 4.85, user: 2.11, sys: 0.24, mem: 508168 ko) +tialL) x + (ZToReg v)) + (withPc + (add (getPc initialL) d) + (withNextPc + (add (getNextPc initialL) d) + initialL))) post -> + FlatToRiscv.runsTo initialL post +assume_riscv_word_properties : forall p : MMIO.parameters, + RiscvWordProperties.word.riscv_ok MMIO.word +COQC bedrock2/compiler/src/examples/EditDistExample.v +COQC bedrock2/compiler/src/examples/swap_bytes_over_uart_hexdump.v +37250200 1305c5fe 03210500 b7850010 93850500 37060040 13060600 9306f001 +3377d100 93070001 3318f700 b3680601 23a01501 13031000 37390110 13098901 +93090027 23203901 373a0110 130a8a00 23206a00 b73a0110 938aca00 23a06a00 +372b0110 130b8b03 b70b0300 938b0b00 23207b01 9303e002 b3007000 33027340 +630c0206 b7020080 93820200 33015000 b3047340 33fc2400 b37c5c00 638c0c00 +373d0110 130d4d00 03210d00 b3846440 6ff05ffe 37340110 13040400 b3015000 +b3047340 b3fd3400 33fe5d00 63080e00 83210400 b3846440 6ff0dffe 23201400 +b3002000 33026240 63967000 33424200 6f004000 6ff0dff8 +make[3]: Leaving directory 'bedrock2/compiler' +make[2]: Leaving directory 'bedrock2/compiler' +COQC Kami/Ex/IsaRv32Pgm.v +COQC Kami/Ex/ProcDec.v +COQC Kami/Ext/Extraction.v +COQC Kami/Tutorial.v +COQC Kami/Ex/ProcThreeStage.v +COQC Kami/Ex/IsaRv32/PgmGcd.v +COQC Kami/Ex/IsaRv32/PgmFact.v +COQC Kami/Ex/IsaRv32/PgmBsort.v +COQC Kami/Ex/IsaRv32/PgmHanoi.v +COQC Kami/Ex/IsaRv32/PgmDekker1.v +COQC Kami/Ex/IsaRv32/PgmDekker2.v +COQC Kami/Ex/IsaRv32/PgmPeterson1.v +COQC Kami/Ex/IsaRv32/PgmPeterson2.v +COQC Kami/Ex/IsaRv32/PgmMatMulInit.v +COQC Kami/Ex/IsaRv32/PgmMatMulNormal1.v +COQC Kami/Ex/IsaRv32/PgmMatMulNormal2.v +COQC Kami/Ex/IsaRv32/PgmMatMulReport.v +COQC Kami/Ex/IsaRv32/PgmBankerInit.v +COQC Kami/Ex/IsaRv32/PgmBankerWorker1.v +COQC Kami/Ex/IsaRv32/PgmBankerWorker2.v +COQC Kami/Ex/IsaRv32/PgmBankerWorker3.v +COQC Kami/Ex/ProcThreeStInl.v +COQC Kami/Ex/ProcFetchDecode.v +COQC Kami/Ex/ProcDecInl.v +COQC Kami/Ex/InDepthTutorial.v +Inductive Modules : Type := + RegFile : string -> + list string -> + string -> + forall (IdxBits : nat) (Data : Kind), + ConstT (Vector Data IdxBits) -> Modules + | Mod : list RegInitT -> + list (Struct.Attribute (Action Void)) -> list DefMethT -> Modules + | ConcatMod : Modules -> Modules -> Modules + +For RegFile: Arguments IdxBits, Data are implicit +For RegFile: Argument scopes are [string_scope list_scope string_scope + nat_scope _ _] +For Mod: Argument scopes are [list_scope list_scope list_scope] +Inductive ActionT (ty : Kind -> Type) (lretT : Kind) : Type := + MCall : string -> + forall s : SignatureT, + (arg s) @ (ty) -> + (ty (ret s) -> ActionT ty lretT) -> ActionT ty lretT + | Let_ : forall lretT' : FullKind, + Expr ty lretT' -> + (fullType ty lretT' -> ActionT ty lretT) -> ActionT ty lretT + | ReadNondet : forall k : FullKind, + (fullType ty k -> ActionT ty lretT) -> ActionT ty lretT + | ReadReg : string -> + forall k : FullKind, + (fullType ty k -> ActionT ty lretT) -> ActionT ty lretT + | WriteReg : string -> + forall k : FullKind, + Expr ty k -> ActionT ty lretT -> ActionT ty lretT + | IfElse : (Bool) @ (ty) -> + forall k : Kind, + ActionT ty k -> + ActionT ty k -> (ty k -> ActionT ty lretT) -> ActionT ty lretT + | Assert_ : (Bool) @ (ty) -> ActionT ty lretT -> ActionT ty lretT + | Displ : list (Disp ty) -> ActionT ty lretT -> ActionT ty lretT + | Return : (lretT) @ (ty) -> ActionT ty lretT + +For MCall: Arguments ty, lretT are implicit +For Let_: Arguments ty, lretT, lretT' are implicit +For ReadNondet: Arguments ty, lretT are implicit +For ReadReg: Arguments ty, lretT are implicit +For WriteReg: Arguments ty, lretT, k are implicit +For IfElse: Arguments ty, lretT, k are implicit +For Assert_: Arguments ty, lretT are implicit +For Displ: Arguments ty, lretT are implicit +For Return: Arguments ty, lretT are implicit +For ActionT: Argument scopes are [function_scope _] +For MCall: Argument scopes are [function_scope _ string_scope _ _ + function_scope] +For Let_: Argument scopes are [function_scope _ _ _ function_scope] +For ReadNondet: Argument scopes are [function_scope _ _ function_scope] +For ReadReg: Argument scopes are [function_scope _ string_scope _ + function_scope] +For WriteReg: Argument scopes are [function_scope _ string_scope _ _ _] +For IfElse: Argument scopes are [function_scope _ _ _ _ _ function_scope] +For Assert_: Argument scopes are [function_scope _ _ _] +For Displ: Argument scopes are [function_scope _ list_scope _] +For Return: Argument scopes are [function_scope _ _] +Inductive Expr (ty : Kind -> Type) : FullKind -> Type := + Var : forall k : FullKind, fullType ty k -> Expr ty k + | Const : forall k : Kind, ConstT k -> (k) @ (ty) + | UniBool : UniBoolOp -> (Bool) @ (ty) -> (Bool) @ (ty) + | BinBool : BinBoolOp -> (Bool) @ (ty) -> (Bool) @ (ty) -> (Bool) @ (ty) + | UniBit : forall n1 n2 : nat, + UniBitOp n1 n2 -> (Bit n1) @ (ty) -> (Bit n2) @ (ty) + | BinBit : forall n1 n2 n3 : nat, + BinBitOp n1 n2 n3 -> + (Bit n1) @ (ty) -> (Bit n2) @ (ty) -> (Bit n3) @ (ty) + | BinBitBool : forall n1 n2 : nat, + BinBitBoolOp n1 n2 -> + (Bit n1) @ (ty) -> (Bit n2) @ (ty) -> (Bool) @ (ty) + | ITE : forall k : FullKind, + (Bool) @ (ty) -> Expr ty k -> Expr ty k -> Expr ty k + | Eq : forall k : Kind, (k) @ (ty) -> (k) @ (ty) -> (Bool) @ (ty) + | ReadIndex : forall (i : nat) (k : Kind), + (Bit i) @ (ty) -> (Vector k i) @ (ty) -> (k) @ (ty) + | ReadField : forall (n : nat) (ls : Vector.t (Struct.Attribute Kind) n) + (i : Fin.t n), + (Struct ls) @ (ty) -> + (Vector.nth (Vector.map (Struct.attrType (A:=Kind)) ls) i) @ + (ty) + | BuildVector : forall (n : Kind) (k : nat), + Vec (n) @ (ty) k -> (Vector n k) @ (ty) + | BuildStruct : forall (n : nat) + (attrs : Vector.t (Struct.Attribute Kind) n), + ilist.ilist + (fun a : Struct.Attribute Kind => + (Struct.attrType a) @ (ty)) attrs -> + (Struct attrs) @ (ty) + | UpdateVector : forall (i : nat) (k : Kind), + (Vector k i) @ (ty) -> + (Bit i) @ (ty) -> (k) @ (ty) -> (Vector k i) @ (ty) + | ReadArrayIndex : forall (i : nat) (k : Kind), + (Bit (Nat.log2 (2 * i))) @ (ty) -> + (Array k i) @ (ty) -> (k) @ (ty) + | BuildArray : forall (n : Kind) (k : nat), + Vector.t (n) @ (ty) (S k) -> (Array n k) @ (ty) + | UpdateArray : forall (i : nat) (k : Kind), + (Array k i) @ (ty) -> + (Bit (Nat.log2 (2 * i))) @ (ty) -> + (k) @ (ty) -> (Array k i) @ (ty) + +For Const: Argument k is implicit +For UniBool: Argument ty is implicit +For BinBool: Argument ty is implicit +For UniBit: Arguments ty, n1, n2 are implicit +For BinBit: Arguments ty, n1, n2, n3 are implicit +For BinBitBool: Arguments ty, n1, n2 are implicit +For ITE: Arguments ty, k are implicit +For Eq: Arguments ty, k are implicit +For ReadIndex: Arguments ty, i, k are implicit +For ReadField: Arguments ty, n, ls are implicit +For BuildVector: Arguments ty, n, k are implicit +For BuildStruct: Arguments ty, n, attrs are implicit +For UpdateVector: Arguments ty, i, k are implicit +For ReadArrayIndex: Arguments ty, i, k are implicit +For BuildArray: Arguments ty, n, k are implicit +For UpdateArray: Arguments ty, i, k are implicit +For Expr: Argument scopes are [function_scope _] +For Var: Argument scopes are [function_scope _ _] +For Const: Argument scopes are [function_scope _ _] +For UniBool: Argument scopes are [function_scope _ _] +For BinBool: Argument scopes are [function_scope _ _ _] +For UniBit: Argument scopes are [function_scope nat_scope nat_scope _ _] +For BinBit: Argument scopes are [function_scope nat_scope nat_scope nat_scope + _ _ _] +For BinBitBool: Argument scopes are [function_scope nat_scope nat_scope _ _ + _] +For ITE: Argument scopes are [function_scope _ _ _ _] +For Eq: Argument scopes are [function_scope _ _ _] +For ReadIndex: Argument scopes are [function_scope nat_scope _ _ _] +For ReadField: Argument scopes are [function_scope nat_scope _ _ _] +For BuildVector: Argument scopes are [function_scope _ nat_scope _] +For BuildStruct: Argument scopes are [function_scope nat_scope _ _] +For UpdateVector: Argument scopes are [function_scope nat_scope _ _ _ _] +For ReadArrayIndex: Argument scopes are [function_scope nat_scope _ _ _] +For BuildArray: Argument scopes are [function_scope _ nat_scope _] +For UpdateArray: Argument scopes are [function_scope nat_scope _ _ _ _] +evalExpr = +fix evalExpr (exprT : FullKind) (e : Expr type exprT) {struct e} : + fullType type exprT := + match e in (Expr _ exprT0) return (fullType type exprT0) with + | @Var _ _ v => v + | @Const _ k v => evalConstT v + | UniBool op e1 => evalUniBool op (evalExpr (SyntaxKind Bool) e1) + | BinBool op e1 e2 => + evalBinBool op (evalExpr (SyntaxKind Bool) e1) + (evalExpr (SyntaxKind Bool) e2) + | @UniBit _ n1 n2 op e1 => + evalUniBit op (evalExpr (SyntaxKind (Bit n1)) e1) + | @BinBit _ n1 n2 n3 op e1 e2 => + evalBinBit op (evalExpr (SyntaxKind (Bit n1)) e1) + (evalExpr (SyntaxKind (Bit n2)) e2) + | @BinBitBool _ n1 n2 op e1 e2 => + evalBinBitBool op (evalExpr (SyntaxKind (Bit n1)) e1) + (evalExpr (SyntaxKind (Bit n2)) e2) + | @ITE _ k p e1 e2 => + if evalExpr (SyntaxKind Bool) p then evalExpr k e1 else evalExpr k e2 + | @Eq _ k e1 e2 => + if isEq k (evalExpr (SyntaxKind k) e1) (evalExpr (SyntaxKind k) e2) + then true + else false + | @ReadIndex _ i0 k i f => + evalExpr (SyntaxKind (Vector k i0)) f + (evalExpr (SyntaxKind (Bit i0)) i) + | @ReadField _ n ls i e0 => + VectorFacts.Vector_nth_map (Struct.attrType (A:=Kind)) type ls + (evalExpr (SyntaxKind (Struct ls)) e0) i + | @BuildVector _ n k vec => evalVec (mapVec (evalExpr (SyntaxKind n)) vec) + | @BuildStruct _ n attrs ils => + ilist.ilist_to_fun_m (Expr type) (fullType type) + (fun sk : Struct.Attribute Kind => SyntaxKind (Struct.attrType sk)) + evalExpr ils + | @UpdateVector _ i0 k fn i v => + fun w : word i0 => + if weq w (evalExpr (SyntaxKind (Bit i0)) i) + then evalExpr (SyntaxKind k) v + else evalExpr (SyntaxKind (Vector k i0)) fn w + | @ReadArrayIndex _ i k idx vec => + evalExpr (SyntaxKind (Array k i)) vec + (natToFin i # (evalExpr (SyntaxKind (Bit (Nat.log2 (2 * i)))) idx)) + | @BuildArray _ i k vecVal => + evalArray (Vector.map (evalExpr (SyntaxKind i)) vecVal) + | @UpdateArray _ i k arr idx val => + fun fini : Fin.t (S i) => + if + Fin.eq_dec fini + (natToFin i # (evalExpr (SyntaxKind (Bit (Nat.log2 (2 * i)))) idx)) + then evalExpr (SyntaxKind k) val + else evalExpr (SyntaxKind (Array k i)) arr fini + end + : forall exprT : FullKind, Expr type exprT -> fullType type exprT + +Argument exprT is implicit +Inductive +SemAction (oldRegs : RegsT) + : forall k : Kind, ActionT type k -> UpdatesT -> MethsT -> type k -> Prop := + SemMCall : forall (meth : M.key) (s : SignatureT) + (marg : (arg s) @ (type)) (mret : type (ret s)) + (retK : Kind) (fret : type retK) + (cont : type (ret s) -> ActionT type retK) + (newRegs : UpdatesT) (calls : MethsT) + (acalls : M.t {x : SignatureT & SignT x}), + (calls) @[ meth]%fmap = None -> + acalls = (calls) #[ meth |-> (evalExpr marg, mret)]%fmap -> + SemAction oldRegs (cont mret) newRegs calls fret -> + SemAction oldRegs (MCall meth s marg cont) newRegs acalls fret + | SemLet : forall (k : FullKind) (e : Expr type k) + (retK : Kind) (fret : type retK) + (cont : fullType type k -> ActionT type retK) + (newRegs : UpdatesT) (calls : MethsT), + SemAction oldRegs (cont (evalExpr e)) newRegs calls fret -> + SemAction oldRegs (LET name <- e; cont name)%kami_action newRegs + calls fret + | SemReadNondet : forall (valueT : FullKind) + (valueV : fullType type valueT) + (retK : Kind) (fret : type retK) + (cont : fullType type valueT -> ActionT type retK) + (newRegs : UpdatesT) (calls : MethsT), + SemAction oldRegs (cont valueV) newRegs calls fret -> + SemAction oldRegs + (Nondet name : valueT; cont name)%kami_action newRegs + calls fret + | SemReadReg : forall (r : string) (regT : FullKind) + (regV : fullType type regT) (retK : Kind) + (fret : type retK) + (cont : fullType type regT -> ActionT type retK) + (newRegs : UpdatesT) (calls : MethsT), + (oldRegs) @[ r]%fmap = + Some (existT (fullType type) regT regV) -> + SemAction oldRegs (cont regV) newRegs calls fret -> + SemAction oldRegs (Read name <- r; cont name)%kami_action + newRegs calls fret + | SemWriteReg : forall (r : string) (k : FullKind) + (e : Expr type k) (retK : Kind) + (fret : type retK) (cont : ActionT type retK) + (newRegs : M.t {x : FullKind & fullType type x}) + (calls : MethsT) + (anewRegs : M.t {x : FullKind & fullType type x}), + (newRegs) @[ r]%fmap = None -> + anewRegs = (newRegs) #[ r |-> evalExpr e]%fmap -> + SemAction oldRegs cont newRegs calls fret -> + SemAction oldRegs (Write r <- e; cont)%kami_action anewRegs + calls fret + | SemIfElseTrue : forall (p : (Bool) @ (type)) (k1 : Kind) + (a a' : ActionT type k1) (r1 : type k1) + (k2 : Kind) (cont : type k1 -> ActionT type k2) + (newRegs1 + newRegs2 : M.Map.t {x : FullKind & fullType type x}) + (calls1 calls2 : M.Map.t {x : SignatureT & SignT x}) + (r2 : type k2), + M.Disj newRegs1 newRegs2 -> + M.Disj calls1 calls2 -> + evalExpr p = true -> + SemAction oldRegs a newRegs1 calls1 r1 -> + SemAction oldRegs (cont r1) newRegs2 calls2 r2 -> + forall + (unewRegs : M.Map.t {x : FullKind & fullType type x}) + (ucalls : M.Map.t {x : SignatureT & SignT x}), + unewRegs = M.union newRegs1 newRegs2 -> + ucalls = M.union calls1 calls2 -> + SemAction oldRegs + (If p then a else a' as name; cont name)%kami_action + unewRegs ucalls r2 + | SemIfElseFalse : forall (p : (Bool) @ (type)) + (k1 : Kind) (a a' : ActionT type k1) + (r1 : type k1) (k2 : Kind) + (cont : type k1 -> ActionT type k2) + (newRegs1 + newRegs2 : M.Map.t {x : FullKind & fullType type x}) + (calls1 calls2 : M.Map.t {x : SignatureT & SignT x}) + (r2 : type k2), + M.Disj newRegs1 newRegs2 -> + M.Disj calls1 calls2 -> + evalExpr p = false -> + SemAction oldRegs a' newRegs1 calls1 r1 -> + SemAction oldRegs (cont r1) newRegs2 calls2 r2 -> + forall + (unewRegs : M.Map.t {x : FullKind & fullType type x}) + (ucalls : M.Map.t {x : SignatureT & SignT x}), + unewRegs = M.union newRegs1 newRegs2 -> + ucalls = M.union calls1 calls2 -> + SemAction oldRegs + (If p then a else a' as name; cont name)%kami_action + unewRegs ucalls r2 + | SemAssertTrue : forall (p : (Bool) @ (type)) (k2 : Kind) + (cont : ActionT type k2) (newRegs2 : UpdatesT) + (calls2 : MethsT) (r2 : type k2), + evalExpr p = true -> + SemAction oldRegs cont newRegs2 calls2 r2 -> + SemAction oldRegs (Assert p; cont)%kami_action newRegs2 + calls2 r2 + | SemDispl : forall (ls : list (Disp type)) (k2 : Kind) + (cont : ActionT type k2) (newRegs2 : UpdatesT) + (calls2 : MethsT) (r2 : type k2), + SemAction oldRegs cont newRegs2 calls2 r2 -> + SemAction oldRegs (Displ ls cont) newRegs2 calls2 r2 + | SemReturn : forall (k : Kind) (e : (k) @ (type)) + (evale : fullType type (SyntaxKind k)), + evale = evalExpr e -> + SemAction oldRegs (Ret e)%kami_action []%fmap []%fmap evale + +For SemAction: Argument k is implicit +For SemMCall: Arguments oldRegs, meth, s, mret, retK, fret, newRegs, calls, + acalls are implicit +For SemLet: Arguments oldRegs, k, retK, fret, newRegs, calls are implicit +For SemReadNondet: Arguments oldRegs, retK, fret, newRegs, calls are implicit +For SemReadReg: Arguments oldRegs, regT, regV, retK, fret, newRegs, calls + are implicit +For SemWriteReg: Arguments oldRegs, r, k, retK, fret, cont, newRegs, calls, + anewRegs are implicit +For SemIfElseTrue: Arguments oldRegs, k1, a, r1, k2, newRegs1, newRegs2, + calls1, calls2, r2, unewRegs, ucalls are implicit +For SemIfElseFalse: Arguments oldRegs, k1, a', r1, k2, newRegs1, newRegs2, + calls1, calls2, r2, unewRegs, ucalls are implicit +For SemAssertTrue: Arguments oldRegs, k2, cont, newRegs2, calls2, r2 + are implicit +For SemDispl: Arguments oldRegs, k2, cont, newRegs2, calls2, r2 are implicit +For SemReturn: Arguments k, evale are implicit +For SemMCall: Argument scopes are [_ _ _ _ _ _ _ function_scope _ _ _ _ _ _] +For SemLet: Argument scopes are [_ _ _ _ _ function_scope _ _ _] +For SemReadNondet: Argument scopes are [_ _ _ _ _ function_scope _ _ _] +For SemReadReg: Argument scopes are [_ string_scope _ _ _ _ function_scope _ + _ _ _] +For SemWriteReg: Argument scopes are [_ string_scope _ _ _ _ _ _ _ _ _ _ _] +For SemIfElseTrue: Argument scopes are [_ _ _ _ _ _ _ function_scope _ _ _ _ + _ _ _ _ _ _ _ _ _ _] +For SemIfElseFalse: Argument scopes are [_ _ _ _ _ _ _ function_scope _ _ _ _ + _ _ _ _ _ _ _ _ _ _] +For SemDispl: Argument scopes are [_ list_scope _ _ _ _ _ _] +Record LabelT : Type := Build_LabelT + { annot : option (option string); defs : MethsT; calls : MethsT } +Inductive +Substep (m : Modules) (o : RegsT) + : UpdatesT -> UnitLabel -> MethsT -> Prop := + EmptyRule : Substep m o []%fmap (Rle None) []%fmap + | EmptyMeth : Substep m o []%fmap (Meth None) []%fmap + | SingleRule : forall (k : string) (a : Action Void), + In (k :: a)%struct (getRules m) -> + forall (u : UpdatesT) (cs : MethsT), + SemAction o (a type) u cs WO -> + Substep m o u (Rle (Some k)) cs + | SingleMeth : forall f : DefMethT, + In f (getDefsBodies m) -> + forall (u : UpdatesT) (cs : MethsT) + (argV : type (arg (projT1 (Struct.attrType f)))) + (retV : type (ret (projT1 (Struct.attrType f)))), + SemAction o (projT2 (Struct.attrType f) type argV) u cs retV -> + forall sig : Struct.Attribute {x : SignatureT & SignT x}, + sig = + (Struct.attrName f + :: existT SignT (projT1 (Struct.attrType f)) (argV, retV))%struct -> + Substep m o u (Meth (Some sig)) cs + +For SingleRule: Arguments o, u, cs are implicit +For SingleMeth: Arguments o, u, cs, argV, retV, sig are implicit +For SingleRule: Argument scopes are [_ _ string_scope _ _ _ _ _] +Inductive +SubstepsInd (m : Modules) (o : RegsT) : UpdatesT -> LabelT -> Prop := + SubstepsNil : SubstepsInd m o []%fmap + {| annot := None; defs := []%fmap; calls := []%fmap |} + | SubstepsCons : forall (u : UpdatesT) (l : LabelT), + SubstepsInd m o u l -> + forall (su : UpdatesT) (scs : MethsT) (sul : UnitLabel), + Substep m o su sul scs -> + CanCombineUUL u l su scs sul -> + forall (uu : M.Map.t {x : FullKind & fullType type x}) + (ll : LabelT), + uu = M.union u su -> + ll = mergeLabel (getLabel sul scs) l -> + SubstepsInd m o uu ll + +For SubstepsCons: Arguments m, o, u, l, su, scs, sul, uu, ll are implicit +Inductive StepInd (m : Modules) (o : RegsT) : UpdatesT -> LabelT -> Prop := + StepIndIntro : forall (u : UpdatesT) (l : LabelT), + SubstepsInd m o u l -> + wellHidden m (hide l) -> StepInd m o u (hide l) + +For StepIndIntro: Arguments m, o, u, l are implicit +Inductive Multistep (m : Modules) : RegsT -> RegsT -> list LabelT -> Prop := + NilMultistep : forall o1 o2 : RegsT, o1 = o2 -> Multistep m o1 o2 nil + | Multi : forall (o : RegsT) (a : list LabelT) (n : RegsT), + Multistep m o n a -> + forall (u : UpdatesT) (l : LabelT), + Step m n u l -> Multistep m o (M.union u n) (l :: a) + +For NilMultistep: Arguments o1, o2 are implicit +For Multi: Arguments m, o, a, n, u, l are implicit +For Multistep: Argument scopes are [_ _ _ list_scope] +For Multi: Argument scopes are [_ _ list_scope _ _ _ _ _] +Inductive Behavior (m : Modules) : RegsT -> LabelSeqT -> Prop := + BehaviorIntro : forall (a : list LabelT) (n : RegsT), + Multistep m (initRegs (getRegInits m)) n a -> + Behavior m n a + +For BehaviorIntro: Arguments m, a, n are implicit +For BehaviorIntro: Argument scopes are [_ list_scope _ _] +traceRefines = +fun (p : MethsT -> MethsT) (m1 m2 : Modules) => +forall (s1 : RegsT) (sig1 : LabelSeqT), +Behavior m1 s1 sig1 -> +exists (s2 : RegsT) (sig2 : LabelSeqT), + Behavior m2 s2 sig2 /\ equivalentLabelSeq p sig1 sig2 + : (MethsT -> MethsT) -> Modules -> Modules -> Prop + +Argument scopes are [function_scope _ _] +traceRefines_refl + : forall m : Modules, traceRefines id m m +traceRefines_trans + : forall (ma mb mc : Modules) (p q : MethsT -> MethsT), + traceRefines p ma mb -> + traceRefines q mb mc -> traceRefines (fun f : MethsT => q (p f)) ma mc +traceRefines_comm + : forall ma mb : Modules, + NoDup (Struct.namesOf (getRegInits (ma ++ mb)%kami)) -> + traceRefines id (ma ++ mb)%kami (mb ++ ma)%kami +traceRefines_assoc_1 + : forall ma mb mc : Modules, + traceRefines id ((ma ++ mb) ++ mc)%kami (ma ++ mb ++ mc)%kami +traceRefines_assoc_2 + : forall ma mb mc : Modules, + traceRefines id (ma ++ mb ++ mc)%kami ((ma ++ mb) ++ mc)%kami +traceRefines_modular_noninteracting + : forall ma mb mc md : Modules, + ModEquiv type typeUT ma -> + ModEquiv type typeUT mb -> + ModEquiv type typeUT mc -> + ModEquiv type typeUT md -> + DisjList (Struct.namesOf (getRegInits ma)) + (Struct.namesOf (getRegInits mc)) -> + DisjList (Struct.namesOf (getRegInits mb)) + (Struct.namesOf (getRegInits md)) -> + ValidRegsModules type (ma ++ mc)%kami -> + ValidRegsModules type (mb ++ md)%kami -> + DisjList (getDefs ma) (getDefs mc) -> + DisjList (getCalls ma) (getCalls mc) -> + DisjList (getDefs mb) (getDefs md) -> + DisjList (getCalls mb) (getCalls md) -> + forall + vp : M.key -> + {x : SignatureT & SignT x} -> option {x : SignatureT & SignT x}, + NonInteracting ma mc -> + NonInteracting mb md -> + (ma <<=[ vp ] mb) -> + (mc <<=[File "./Kami/Ex/InDepthTutorial.v", line 229, characters 0-58: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 232, characters 0-26: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 241, characters 0-55: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 245, characters 0-25: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 274, characters 0-30: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 277, characters 0-29: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 357, characters 0-28: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 360, characters 0-27: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 379, characters 0-28: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 382, characters 0-27: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 408, characters 0-334: +Warning: +datav cannot be defined because it is informative and impl12_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 408, characters 0-334: +Warning: +Hdatav cannot be defined because the projection datav was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 408, characters 0-334: +Warning: +eltv cannot be defined because it is informative and impl12_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 408, characters 0-334: +Warning: Heltv cannot be defined because the projection eltv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 408, characters 0-334: +Warning: +Hinv cannot be defined because the projections eltv, datav were not defined. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 527, characters 0-29: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 530, characters 0-28: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 554, characters 0-33: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/InDepthTutorial.v", line 557, characters 0-343: +Warning: +datav cannot be defined because it is informative and impl123_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 557, characters 0-343: +Warning: +Hdatav cannot be defined because the projection datav was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 557, characters 0-343: +Warning: +eltv cannot be defined because it is informative and impl123_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 557, characters 0-343: +Warning: Heltv cannot be defined because the projection eltv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/InDepthTutorial.v", line 557, characters 0-343: +Warning: +Hinv cannot be defined because the projections eltv, datav were not defined. +[cannot-define-projection,records] +Kami/Ex/ProcDecInl (real: 36.23, user: 17.33, sys: 0.37, mem: 724164 ko) +Kami/Ex/IsaRv32PgmExt (real: 2.54, user: 0.92, sys: 0.31, mem: 550756 ko) +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +sbv0 cannot be defined because it is informative and p3st_scoreboard_waw_inv +is not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: Hsbv0 cannot be defined because the projection sbv0 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +d2eeltv0 cannot be defined because it is informative and +p3st_scoreboard_waw_inv is not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +Hd2eeltv0 cannot be defined because the projection d2eeltv0 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +d2efullv0 cannot be defined because it is informative and +p3st_scoreboard_waw_inv is not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +Hd2efullv0 cannot be defined because the projection d2efullv0 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +e2weltv0 cannot be defined because it is informative and +p3st_scoreboard_waw_inv is not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +He2weltv0 cannot be defined because the projection e2weltv0 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +e2wfullv0 cannot be defined because it is informative and +p3st_scoreboard_waw_inv is not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +He2wfullv0 cannot be defined because the projection e2wfullv0 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +stallv0 cannot be defined because it is informative and +p3st_scoreboard_waw_inv is not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +Hstallv0 cannot be defined because the projection stallv0 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +stalledv0 cannot be defined because it is informative and +p3st_scoreboard_waw_inv is not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +Hstalledv0 cannot be defined because the projection stalledv0 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 155, characters 2-1108: +Warning: +Hinv0 cannot be defined because the projections d2efullv0, d2eeltv0, +e2wfullv0, e2weltv0, stallv0, stalledv0, sbv0 were not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +d2eeltv1 cannot be defined because it is informative and p3st_raw_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +Hd2eeltv1 cannot be defined because the projection d2eeltv1 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +d2efullv1 cannot be defined because it is informative and p3st_raw_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +Hd2efullv1 cannot be defined because the projection d2efullv1 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +e2weltv1 cannot be defined because it is informative and p3st_raw_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +He2weltv1 cannot be defined because the projection e2weltv1 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +e2wfullv1 cannot be defined because it is informative and p3st_raw_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +He2wfullv1 cannot be defined because the projection e2wfullv1 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +stallv1 cannot be defined because it is informative and p3st_raw_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +Hstallv1 cannot be defined because the projection stallv1 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +stalledv1 cannot be defined because it is informative and p3st_raw_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +Hstalledv1 cannot be defined because the projection stalledv1 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +Hd2einv1 cannot be defined because the projections d2efullv1, stallv1, +d2eeltv1, stalledv1 were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +He2winv1 cannot be defined because the projections e2wfullv1, stallv1, +e2weltv1, stalledv1 were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 192, characters 2-1091: +Warning: +Hd2winv1 cannot be defined because the projections d2efullv1, e2wfullv1, +d2eeltv1, e2weltv1 were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +pgmv2 cannot be defined because it is informative and p3st_decode_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +Hpgmv2 cannot be defined because the projection pgmv2 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +rfv2 cannot be defined because it is informative and p3st_decode_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: Hrfv2 cannot be defined because the projection rfv2 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +d2eeltv2 cannot be defined because it is informative and p3st_decode_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +Hd2eeltv2 cannot be defined because the projection d2eeltv2 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +d2efullv2 cannot be defined because it is informative and p3st_decode_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +Hd2efullv2 cannot be defined because the projection d2efullv2 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +e2weltv2 cannot be defined because it is informative and p3st_decode_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +He2weltv2 cannot be defined because the projection e2weltv2 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +e2wfullv2 cannot be defined because it is informative and p3st_decode_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +He2wfullv2 cannot be defined because the projection e2wfullv2 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +Hd2einv2 cannot be defined because the projections pgmv2, rfv2, d2eeltv2, +d2efullv2 were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 238, characters 2-1015: +Warning: +He2winv2 cannot be defined because the projections pgmv2, rfv2, e2weltv2, +e2wfullv2 were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +pgmv3 cannot be defined because it is informative and p3st_stalled_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +Hpgmv3 cannot be defined because the projection pgmv3 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +rfv3 cannot be defined because it is informative and p3st_stalled_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: Hrfv3 cannot be defined because the projection rfv3 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +stallv3 cannot be defined because it is informative and p3st_stalled_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +Hstallv3 cannot be defined because the projection stallv3 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +stalledv3 cannot be defined because it is informative and p3st_stalled_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +Hstalledv3 cannot be defined because the projection stalledv3 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 272, characters 2-641: +Warning: +Hinv3 cannot be defined because the projections pgmv3, rfv3, stallv3, +stalledv3 were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: +pcv4 cannot be defined because it is informative and p3st_exec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: Hpcv4 cannot be defined because the projection pcv4 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: +rfv4 cannot be defined because it is informative and p3st_exec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: Hrfv4 cannot be defined because the projection rfv4 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: +e2weltv4 cannot be defined because it is informative and p3st_exec_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: +He2weltv4 cannot be defined because the projection e2weltv4 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: +e2wfullv4 cannot be defined because it is informative and p3st_exec_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: +He2wfullv4 cannot be defined because the projection e2wfullv4 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 299, characters 2-621: +Warning: +Hinv4 cannot be defined because the projections pcv4, rfv4, e2wfullv4, +e2weltv4 were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +pcv5 cannot be defined because it is informative and p3st_epochs_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: Hpcv5 cannot be defined because the projection pcv5 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +fepochv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hfepochv5 cannot be defined because the projection fepochv5 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +d2eeltv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hd2eeltv5 cannot be defined because the projection d2eeltv5 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +d2efullv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hd2efullv5 cannot be defined because the projection d2efullv5 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +w2deltv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hw2deltv5 cannot be defined because the projection w2deltv5 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +w2dfullv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hw2dfullv5 cannot be defined because the projection w2dfullv5 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +e2weltv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +He2weltv5 cannot be defined because the projection e2weltv5 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +e2wfullv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +He2wfullv5 cannot be defined because the projection e2wfullv5 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +stallv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hstallv5 cannot be defined because the projection stallv5 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +stalledv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hstalledv5 cannot be defined because the projection stalledv5 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +eepochv5 cannot be defined because it is informative and p3st_epochs_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Heepochv5 cannot be defined because the projection eepochv5 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 340, characters 2-1704: +Warning: +Hinv5 cannot be defined because the projections fepochv5, eepochv5, +d2efullv5, e2wfullv5, w2dfullv5, stallv5, pcv5, d2eeltv5, e2weltv5, stalledv5 +were not defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +pcv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: Hpcv6 cannot be defined because the projection pcv6 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +fepochv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Hfepochv6 cannot be defined because the projection fepochv6 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +d2eeltv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Hd2eeltv6 cannot be defined because the projection d2eeltv6 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +d2efullv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Hd2efullv6 cannot be defined because the projection d2efullv6 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +w2dfullv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Hw2dfullv6 cannot be defined because the projection w2dfullv6 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +e2weltv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +He2weltv6 cannot be defined because the projection e2weltv6 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +e2wfullv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +He2wfullv6 cannot be defined because the projection e2wfullv6 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +stallv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Hstallv6 cannot be defined because the projection stallv6 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +stalledv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Hstalledv6 cannot be defined because the projection stalledv6 was not +defined. [cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +eepochv6 cannot be defined because it is informative and p3st_pc_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Heepochv6 cannot be defined because the projection eepochv6 was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcThreeStInv.v", line 398, characters 2-1469: +Warning: +Hinv6 cannot be defined because the projections fepochv6, eepochv6, +d2efullv6, e2wfullv6, w2dfullv6, stallv6, pcv6, d2eeltv6, e2weltv6, stalledv6 +were not defined. [cannot-define-projection,records] +Kami/Ex/ProcThreeStInv (real: 3.48, user: 1.44, sys: 0.25, mem: 498104 ko) +File "./Kami/Ex/InDepthTutorial.v", line 680, characters 0-16: +Warning: The spelling "OCaml" should be used instead of "Ocaml". +[deprecated-ocaml-spelling,deprecated] +Kami/Ex/InDepthTutorial (real: 47.16, user: 22.68, sys: 0.34, mem: 653084 ko) +File "./Kami/Ex/ProcThreeStDec.v", line 120, characters 2-59: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcThreeStDec.v", line 121, characters 2-59: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/ProcThreeStDec (real: 2.97, user: 1.19, sys: 0.25, mem: 495240 ko) +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +pcv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: Hpcv cannot be defined because the projection pcv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +rfv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: Hrfv cannot be defined because the projection rfv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +pgmv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: Hpgmv cannot be defined because the projection pgmv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +stallv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hstallv cannot be defined because the projection stallv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +iev cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: Hiev cannot be defined because the projection iev was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +ifv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: Hifv cannot be defined because the projection ifv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +ienqpv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hienqpv cannot be defined because the projection ienqpv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +ideqpv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hideqpv cannot be defined because the projection ideqpv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +ieltv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hieltv cannot be defined because the projection ieltv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +oev cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: Hoev cannot be defined because the projection oev was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +ofv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: Hofv cannot be defined because the projection ofv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +oenqpv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hoenqpv cannot be defined because the projection oenqpv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +odeqpv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hodeqpv cannot be defined because the projection odeqpv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +oeltv cannot be defined because it is informative and procDec_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hoeltv cannot be defined because the projection oeltv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcDecInv.v", line 82, characters 2-2422: +Warning: +Hinv cannot be defined because the projections stallv, iev, ienqpv, ideqpv, +oev, oenqpv, odeqpv, stallv, iev, ienqpv, ideqpv, oev, oenqpv, odeqpv, pgmv, +pcv, rfv, iev, ieltv, ideqpv, stallv, iev, ienqpv, ideqpv, oev, oenqpv, +odeqpv were not defined. [cannot-define-projection,records] +Kami/Ex/ProcDecInv (real: 4.24, user: 1.78, sys: 0.26, mem: 495196 ko) +File "./Kami/Ex/ProcDecSC.v", line 46, characters 2-59: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcDecSC.v", line 47, characters 2-61: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/ProcDecSC (real: 4.07, user: 0.93, sys: 0.30, mem: 493232 ko) +Kami/Ex/ProcDecSCN (real: 2.30, user: 0.81, sys: 0.29, mem: 488468 ko) +Kami/Ex/ProcFDInl (real: 81.62, user: 68.57, sys: 0.68, mem: 1312068 ko) +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +pcv cannot be defined because it is informative and fetchDecode_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: Hpcv cannot be defined because the projection pcv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +pgmv cannot be defined because it is informative and fetchDecode_inv is not. +[cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: Hpgmv cannot be defined because the projection pgmv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +fepochv cannot be defined because it is informative and fetchDecode_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +Hfepochv cannot be defined because the projection fepochv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +f2dfullv cannot be defined because it is informative and fetchDecode_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +Hf2dfullv cannot be defined because the projection f2dfullv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +f2deltv cannot be defined because it is informative and fetchDecode_inv is +not. [cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +Hf2deltv cannot be defined because the projection f2deltv was not defined. +[cannot-define-projection,records] +File "./Kami/Ex/ProcFDInv.v", line 103, characters 2-743: +Warning: +Hinv cannot be defined because the projections pcv, pgmv, fepochv, f2dfullv, +f2deltv were not defined. [cannot-define-projection,records] +Kami/Ex/ProcFDInv (real: 2.76, user: 2.42, sys: 0.23, mem: 526316 ko) +File "./Kami/Ex/ProcFDCorrect.v", line 96, characters 2-73: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +File "./Kami/Ex/ProcFDCorrect.v", line 97, characters 2-75: +Warning: Adding and removing hints in the core database implicitly is +deprecated. Please specify a hint database. +[implicit-core-hint-db,deprecated] +Kami/Ex/ProcFDCorrect (real: 1.11, user: 0.83, sys: 0.23, mem: 526908 ko) +Kami/Ex/ProcFourStDec (real: 1.06, user: 0.80, sys: 0.23, mem: 527136 ko) +Warning: bedrock2/deps/coqutil/src (used in -R or -Q) is not a subdirectory of the current directory + +bedrock2/processor/src/KamiWord (real: 1.30, user: 0.45, sys: 0.16, mem: 358800 ko) +bedrock2/processor/src/Test (real: 3.56, user: 1.51, sys: 0.22, mem: 473632 ko) +bedrock2/processor/src/KamiRiscv (real: 27.54, user: 25.47, sys: 0.35, mem: 729768 ko) + vp ] md) -> (ma ++ mc)%kami <<=[ vp ] (mb ++ md)%kami +simpleFifo + : string -> nat -> Kind -> Modules + = Mod + [("data" :: RegInitDefault (SyntaxKind (Bit dataSize)))%struct; + ("elt.fifo1" + :: RegInitCustom + (existT ConstFullT (list (word dataSize)) #< (nil)%kami_expr + (NativeConst nil nil)))%struct] + [("produce" + :: (fun type : Kind -> Type => + (Read a : Bit dataSize <- "data"; + LET a0 : Bit dataSize <- # (a); + Read a1 <- "elt.fifo1"; + Write "elt.fifo1" <- + Var type (list (type (Bit dataSize))) #< (nil) + ((fix app (l m : list (type (Bit dataSize))) {struct l} : + list (type (Bit dataSize)) := + match l with + | nil => m + | a2 :: l1 => a2 :: app l1 m + end) a1 [a0]); + LET _ : Void <- $$ (WO); + Write "data" : Bit dataSize <- # (a) + $$ ($ (1)); + Ret $$ (WO))%kami_action))%struct; + ("doDouble" + :: (fun type : Kind -> Type => + (LET _ : Void <- $$ (WO); + Read a0 <- "elt.fifo1"; + Assert ! + $$ + (match a0 with + | nil => true + | _ :: _ => false + end); + Write "elt.fifo1" <- + Var type (list (type (Bit dataSize))) #< (nil) + match a0 with + | nil => nil + | _ :: t => t + end; + LET ak : Bit dataSize <- + match a0 with + | nil => $$ (getDefaultConstBit dataSize) + | h :: _ => # (h) + end; + LET a1 : Bit dataSize <- $$ ($ (2)) * # (ak); + CallM _ : Void <- "enq.fifo2" (# (a1) : + Bit dataSize); Ret $$ (WO))%kami_action))%struct] nil + : Modules +COQC Kami/Ex/IsaRv32PgmExt.v +COQC Kami/Ex/ProcThreeStInv.v +COQC Kami/Ex/ProcFDInl.v +impl = +fun dataSize : nat => +(stage1 dataSize ++ + fifo1 dataSize ++ stage2 dataSize ++ fifo2 dataSize ++ stage3 dataSize)%kami + : nat -> Modules + +Argument scope is [nat_scope] +COQC Kami/Ex/ProcThreeStDec.v +COQC Kami/Ex/ProcDecInv.v +COQC Kami/Ex/ProcDecSC.v +COQC Kami/Ex/ProcDecSCN.v +COQC Kami/Ex/ProcFDInv.v +COQC Kami/Ex/ProcFDCorrect.v +COQC Kami/Ex/ProcFourStDec.v +make[3]: Leaving directory 'bedrock2/deps/kami' +make[2]: Leaving directory 'bedrock2/deps/kami' +make -C bedrock2/processor +make[2]: Entering directory 'bedrock2/processor' +printf -- '-Q bedrock2/deps/coqutil/src coqutil\n-Q bedrock2/deps/riscv-coq/src riscv\n-R bedrock2/deps/kami/Kami/ Kami\n-Q ./src processor\n' > _CoqProject +/builds/coq/coq/_install_ci/bin/coq_makefile -f _CoqProject INSTALLDEFAULTROOT = bedrock2 -arg "-async-proofs-tac-j 1" bedrock2/processor/src/Test.v bedrock2/processor/src/KamiWord.v bedrock2/processor/src/KamiRiscv.v -o Makefile.coq.all +make -f Makefile.coq.all +make[3]: Entering directory 'bedrock2/processor' +COQDEP VFILES +COQC bedrock2/processor/src/Test.v +COQC bedrock2/processor/src/KamiWord.v +COQC bedrock2/processor/src/KamiRiscv.v +make[3]: Leaving directory 'bedrock2/processor' +make[2]: Leaving directory 'bedrock2/processor' +make[1]: Leaving directory 'bedrock2' diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 0c5fdb50ac..3d07661d56 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -34,6 +34,24 @@ def reformat_time_string(time): minutes, seconds = divmod(seconds, 60) return '%dm%02d.%ss' % (minutes, seconds, milliseconds) +def get_file_lines(file_name): + if file_name == '-': + if hasattr(sys.stdin, 'buffer'): + lines = sys.stdin.buffer.readlines() + else: + lines = sys.stdin.readlines() + else: + with open(file_name, 'rb') as f: + lines = f.readlines() + for line in lines: + try: + yield line.decode('utf-8') + except UnicodeDecodeError: # invalid utf-8 + pass + +def get_file(file_name): + return ''.join(get_file_lines(file_name)) + def get_times(file_name): ''' Reads the contents of file_name, which should be the output of @@ -41,11 +59,7 @@ def get_times(file_name): names to compile durations, as strings. Removes common prefixes using STRIP_REG and STRIP_REP. ''' - if file_name == '-': - lines = sys.stdin.read() - else: - with open(file_name, 'r', encoding="utf-8") as f: - lines = f.read() + lines = get_file(file_name) reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) if all(time in ('0.00', '0.01') for name, time in times): @@ -61,11 +75,7 @@ def get_single_file_times(file_name): 'coqc -time', and parses it to construct a dict mapping lines to to compile durations, as strings. ''' - if file_name == '-': - lines = sys.stdin.read() - else: - with open(file_name, 'r', encoding="utf-8") as f: - lines = f.read() + lines = get_file(file_name) reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) times = reg.findall(lines) if len(times) == 0: return dict() @@ -212,7 +222,7 @@ def print_or_write_table(table, files): if hasattr(sys.stdout, 'buffer'): sys.stdout.buffer.write(table.encode("utf-8")) else: - sys.stdout.write(table) + sys.stdout.write(table.encode("utf-8")) for file_name in files: if file_name != '-': with open(file_name, 'w', encoding="utf-8") as f: |