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'
