COQDEP src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v COQDEP src/Compilers/Z/Bounds/Pipeline/Definition.v /home/jgross/.local64/coq/coq-master/bin/coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-old COQ_MAKEFILE -f _CoqProject > Makefile.coq make --no-print-directory -C coqprime make[1]: Nothing to be done for 'all'. ECHO > _CoqProject COQC src/Compilers/Z/Bounds/Pipeline/Definition.v src/Compilers/Z/Bounds/Pipeline/Definition (real: 7.33, user: 7.18, sys: 0.14, mem: 574388 ko) COQC src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics (real: 1.93, user: 1.72, sys: 0.20, mem: 544172 ko) COQC src/Compilers/Z/Bounds/Pipeline.v src/Compilers/Z/Bounds/Pipeline (real: 1.38, user: 1.19, sys: 0.16, mem: 539808 ko) COQC src/Specific/Framework/SynthesisFramework.v src/Specific/Framework/SynthesisFramework (real: 1.85, user: 1.67, sys: 0.17, mem: 646300 ko) COQC src/Specific/X25519/C64/Synthesis.v src/Specific/X25519/C64/Synthesis (real: 11.15, user: 10.37, sys: 0.18, mem: 687760 ko) COQC src/Specific/NISTP256/AMD64/Synthesis.v src/Specific/NISTP256/AMD64/Synthesis (real: 13.45, user: 12.55, sys: 0.19, mem: 668216 ko) COQC src/Specific/X25519/C64/feadd.v Finished transaction in 2.814 secs (2.624u,0.s) (successful) total time: 2.576s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.2% 97.4% 1 2.508s ─ReflectiveTactics.do_reflective_pipelin 0.0% 66.9% 1 1.724s ─ReflectiveTactics.solve_side_conditions 0.0% 65.5% 1 1.688s ─ReflectiveTactics.solve_post_reified_si 1.2% 37.0% 1 0.952s ─Glue.refine_to_reflective_glue' ------- 0.0% 30.3% 1 0.780s ─ReflectiveTactics.do_reify ------------ 0.0% 28.6% 1 0.736s ─Reify.Reify_rhs_gen ------------------- 2.2% 26.6% 1 0.684s ─UnifyAbstractReflexivity.unify_transfor 20.3% 24.1% 7 0.164s ─Glue.zrange_to_reflective ------------- 0.0% 20.3% 1 0.524s ─Glue.zrange_to_reflective_goal -------- 9.5% 15.2% 1 0.392s ─Reify.do_reify_abs_goal --------------- 13.7% 13.8% 2 0.356s ─Reify.do_reifyf_goal ------------------ 12.4% 12.6% 16 0.324s ─ReflectiveTactics.unify_abstract_cbv_in 8.4% 11.2% 1 0.288s ─unify (constr) (constr) --------------- 5.7% 5.7% 6 0.072s ─Glue.pattern_sig_sig_assoc ------------ 0.0% 5.4% 1 0.140s ─assert (H : is_bounded_by' bounds (map' 4.8% 5.1% 2 0.072s ─Glue.pattern_proj1_sig_in_sig --------- 1.7% 5.1% 1 0.132s ─pose proof (pf : Interpretation.Bo 3.7% 3.7% 1 0.096s ─Glue.split_BoundedWordToZ ------------- 0.3% 3.7% 1 0.096s ─destruct_sig -------------------------- 0.2% 3.3% 4 0.044s ─destruct x ---------------------------- 3.1% 3.1% 4 0.036s ─eexact -------------------------------- 3.0% 3.0% 18 0.008s ─clearbody (ne_var_list) --------------- 3.0% 3.0% 4 0.060s ─prove_interp_compile_correct ---------- 0.0% 2.8% 1 0.072s ─synthesize ---------------------------- 0.0% 2.6% 1 0.068s ─rewrite ?EtaInterp.InterpExprEta ------ 2.5% 2.5% 1 0.064s ─ClearbodyAll.clearbody_all ------------ 0.0% 2.3% 2 0.060s ─rewrite H ----------------------------- 2.2% 2.2% 1 0.056s ─reflexivity --------------------------- 2.2% 2.2% 7 0.032s ─Reify.transitivity_tt ----------------- 0.0% 2.2% 2 0.032s ─transitivity -------------------------- 2.0% 2.0% 5 0.024s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.2% 97.4% 1 2.508s ├─ReflectiveTactics.do_reflective_pipel 0.0% 66.9% 1 1.724s │└ReflectiveTactics.solve_side_conditio 0.0% 65.5% 1 1.688s │ ├─ReflectiveTactics.solve_post_reifie 1.2% 37.0% 1 0.952s │ │ ├─UnifyAbstractReflexivity.unify_tr 20.3% 24.1% 7 0.164s │ │ │└unify (constr) (constr) --------- 3.0% 3.0% 5 0.028s │ │ └─ReflectiveTactics.unify_abstract_ 8.4% 11.2% 1 0.288s │ │ └unify (constr) (constr) --------- 2.8% 2.8% 1 0.072s │ └─ReflectiveTactics.do_reify -------- 0.0% 28.6% 1 0.736s │ └Reify.Reify_rhs_gen --------------- 2.2% 26.6% 1 0.684s │ ├─Reify.do_reify_abs_goal --------- 13.7% 13.8% 2 0.356s │ │└Reify.do_reifyf_goal ------------ 12.4% 12.6% 16 0.324s │ │└eexact -------------------------- 2.6% 2.6% 16 0.008s │ ├─prove_interp_compile_correct ---- 0.0% 2.8% 1 0.072s │ │└rewrite ?EtaInterp.InterpExprEta 2.5% 2.5% 1 0.064s │ ├─rewrite H ----------------------- 2.2% 2.2% 1 0.056s │ └─Reify.transitivity_tt ----------- 0.0% 2.2% 2 0.032s └─Glue.refine_to_reflective_glue' ----- 0.0% 30.3% 1 0.780s ├─Glue.zrange_to_reflective --------- 0.0% 20.3% 1 0.524s │ ├─Glue.zrange_to_reflective_goal -- 9.5% 15.2% 1 0.392s │ │└pose proof (pf : Interpretat 3.7% 3.7% 1 0.096s │ └─assert (H : is_bounded_by' bounds 4.8% 5.1% 2 0.072s ├─Glue.pattern_sig_sig_assoc -------- 0.0% 5.4% 1 0.140s │└Glue.pattern_proj1_sig_in_sig ----- 1.7% 5.1% 1 0.132s │└ClearbodyAll.clearbody_all -------- 0.0% 2.3% 2 0.060s │└clearbody (ne_var_list) ----------- 2.3% 2.3% 1 0.060s └─Glue.split_BoundedWordToZ --------- 0.3% 3.7% 1 0.096s └destruct_sig ---------------------- 0.2% 3.3% 4 0.044s └destruct x ------------------------ 2.5% 2.5% 2 0.036s ─synthesize ---------------------------- 0.0% 2.6% 1 0.068s Finished transaction in 5.021 secs (4.636u,0.s) (successful) Closed under the global context total time: 2.576s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.2% 97.4% 1 2.508s ─ReflectiveTactics.do_reflective_pipelin 0.0% 66.9% 1 1.724s ─ReflectiveTactics.solve_side_conditions 0.0% 65.5% 1 1.688s ─ReflectiveTactics.solve_post_reified_si 1.2% 37.0% 1 0.952s ─Glue.refine_to_reflective_glue' ------- 0.0% 30.3% 1 0.780s ─ReflectiveTactics.do_reify ------------ 0.0% 28.6% 1 0.736s ─Reify.Reify_rhs_gen ------------------- 2.2% 26.6% 1 0.684s ─UnifyAbstractReflexivity.unify_transfor 20.3% 24.1% 7 0.164s ─Glue.zrange_to_reflective ------------- 0.0% 20.3% 1 0.524s ─Glue.zrange_to_reflective_goal -------- 9.5% 15.2% 1 0.392s ─Reify.do_reify_abs_goal --------------- 13.7% 13.8% 2 0.356s ─Reify.do_reifyf_goal ------------------ 12.4% 12.6% 16 0.324s ─ReflectiveTactics.unify_abstract_cbv_in 8.4% 11.2% 1 0.288s ─unify (constr) (constr) --------------- 5.7% 5.7% 6 0.072s ─Glue.pattern_sig_sig_assoc ------------ 0.0% 5.4% 1 0.140s ─assert (H : is_bounded_by' bounds (map' 4.8% 5.1% 2 0.072s ─Glue.pattern_proj1_sig_in_sig --------- 1.7% 5.1% 1 0.132s ─pose proof (pf : Interpretation.Bo 3.7% 3.7% 1 0.096s ─Glue.split_BoundedWordToZ ------------- 0.3% 3.7% 1 0.096s ─destruct_sig -------------------------- 0.2% 3.3% 4 0.044s ─destruct x ---------------------------- 3.1% 3.1% 4 0.036s ─eexact -------------------------------- 3.0% 3.0% 18 0.008s ─clearbody (ne_var_list) --------------- 3.0% 3.0% 4 0.060s ─prove_interp_compile_correct ---------- 0.0% 2.8% 1 0.072s ─synthesize ---------------------------- 0.0% 2.6% 1 0.068s ─rewrite ?EtaInterp.InterpExprEta ------ 2.5% 2.5% 1 0.064s ─ClearbodyAll.clearbody_all ------------ 0.0% 2.3% 2 0.060s ─rewrite H ----------------------------- 2.2% 2.2% 1 0.056s ─reflexivity --------------------------- 2.2% 2.2% 7 0.032s ─Reify.transitivity_tt ----------------- 0.0% 2.2% 2 0.032s ─transitivity -------------------------- 2.0% 2.0% 5 0.024s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.2% 97.4% 1 2.508s ├─ReflectiveTactics.do_reflective_pipel 0.0% 66.9% 1 1.724s │└ReflectiveTactics.solve_side_conditio 0.0% 65.5% 1 1.688s │ ├─ReflectiveTactics.solve_post_reifie 1.2% 37.0% 1 0.952s │ │ ├─UnifyAbstractReflexivity.unify_tr 20.3% 24.1% 7 0.164s │ │ │└unify (constr) (constr) --------- 3.0% 3.0% 5 0.028s │ │ └─ReflectiveTactics.unify_abstract_ 8.4% 11.2% 1 0.288s │ │ └unify (constr) (constr) --------- 2.8% 2.8% 1 0.072s │ └─ReflectiveTactics.do_reify -------- 0.0% 28.6% 1 0.736s │ └Reify.Reify_rhs_gen --------------- 2.2% 26.6% 1 0.684s │ ├─Reify.do_reify_abs_goal --------- 13.7% 13.8% 2 0.356s │ │└Reify.do_reifyf_goal ------------ 12.4% 12.6% 16 0.324s │ │└eexact -------------------------- 2.6% 2.6% 16 0.008s │ ├─prove_interp_compile_correct ---- 0.0% 2.8% 1 0.072s │ │└rewrite ?EtaInterp.InterpExprEta 2.5% 2.5% 1 0.064s │ ├─rewrite H ----------------------- 2.2% 2.2% 1 0.056s │ └─Reify.transitivity_tt ----------- 0.0% 2.2% 2 0.032s └─Glue.refine_to_reflective_glue' ----- 0.0% 30.3% 1 0.780s ├─Glue.zrange_to_reflective --------- 0.0% 20.3% 1 0.524s │ ├─Glue.zrange_to_reflective_goal -- 9.5% 15.2% 1 0.392s │ │└pose proof (pf : Interpretat 3.7% 3.7% 1 0.096s │ └─assert (H : is_bounded_by' bounds 4.8% 5.1% 2 0.072s ├─Glue.pattern_sig_sig_assoc -------- 0.0% 5.4% 1 0.140s │└Glue.pattern_proj1_sig_in_sig ----- 1.7% 5.1% 1 0.132s │└ClearbodyAll.clearbody_all -------- 0.0% 2.3% 2 0.060s │└clearbody (ne_var_list) ----------- 2.3% 2.3% 1 0.060s └─Glue.split_BoundedWordToZ --------- 0.3% 3.7% 1 0.096s └destruct_sig ---------------------- 0.2% 3.3% 4 0.044s └destruct x ------------------------ 2.5% 2.5% 2 0.036s ─synthesize ---------------------------- 0.0% 2.6% 1 0.068s src/Specific/X25519/C64/feadd (real: 22.81, user: 20.93, sys: 0.25, mem: 766300 ko) COQC src/Specific/X25519/C64/fecarry.v Finished transaction in 4.343 secs (4.016u,0.004s) (successful) total time: 3.976s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 99.0% 1 3.936s ─ReflectiveTactics.do_reflective_pipelin 0.0% 87.9% 1 3.496s ─ReflectiveTactics.solve_side_conditions 0.0% 86.9% 1 3.456s ─ReflectiveTactics.do_reify ------------ 0.0% 56.9% 1 2.264s ─Reify.Reify_rhs_gen ------------------- 1.8% 56.2% 1 2.236s ─Reify.do_reify_abs_goal --------------- 36.1% 36.5% 2 1.452s ─Reify.do_reifyf_goal ------------------ 34.8% 35.1% 29 1.396s ─ReflectiveTactics.solve_post_reified_si 0.6% 30.0% 1 1.192s ─UnifyAbstractReflexivity.unify_transfor 17.7% 21.7% 7 0.240s ─Glue.refine_to_reflective_glue' ------- 0.0% 11.1% 1 0.440s ─eexact -------------------------------- 10.9% 10.9% 31 0.024s ─ReflectiveTactics.unify_abstract_cbv_in 5.2% 7.3% 1 0.292s ─Glue.zrange_to_reflective ------------- 0.0% 7.1% 1 0.284s ─prove_interp_compile_correct ---------- 0.0% 5.7% 1 0.228s ─Glue.zrange_to_reflective_goal -------- 4.3% 5.5% 1 0.220s ─unify (constr) (constr) --------------- 5.3% 5.3% 6 0.084s ─rewrite ?EtaInterp.InterpExprEta ------ 5.2% 5.2% 1 0.208s ─rewrite H ----------------------------- 3.5% 3.5% 1 0.140s ─tac ----------------------------------- 1.9% 2.6% 2 0.104s ─reflexivity --------------------------- 2.2% 2.2% 7 0.028s ─Reify.transitivity_tt ----------------- 0.0% 2.2% 2 0.056s ─transitivity -------------------------- 2.0% 2.0% 5 0.048s ─Glue.split_BoundedWordToZ ------------- 0.1% 2.0% 1 0.080s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 99.0% 1 3.936s ├─ReflectiveTactics.do_reflective_pipel 0.0% 87.9% 1 3.496s │└ReflectiveTactics.solve_side_conditio 0.0% 86.9% 1 3.456s │ ├─ReflectiveTactics.do_reify -------- 0.0% 56.9% 1 2.264s │ │└Reify.Reify_rhs_gen --------------- 1.8% 56.2% 1 2.236s │ │ ├─Reify.do_reify_abs_goal --------- 36.1% 36.5% 2 1.452s │ │ │└Reify.do_reifyf_goal ------------ 34.8% 35.1% 29 1.396s │ │ │└eexact -------------------------- 10.1% 10.1% 29 0.024s │ │ ├─prove_interp_compile_correct ---- 0.0% 5.7% 1 0.228s │ │ │└rewrite ?EtaInterp.InterpExprEta 5.2% 5.2% 1 0.208s │ │ ├─rewrite H ----------------------- 3.5% 3.5% 1 0.140s │ │ ├─tac ----------------------------- 1.9% 2.6% 1 0.104s │ │ └─Reify.transitivity_tt ----------- 0.0% 2.2% 2 0.056s │ │ └transitivity -------------------- 2.0% 2.0% 4 0.048s │ └─ReflectiveTactics.solve_post_reifie 0.6% 30.0% 1 1.192s │ ├─UnifyAbstractReflexivity.unify_tr 17.7% 21.7% 7 0.240s │ │└unify (constr) (constr) --------- 3.2% 3.2% 5 0.048s │ └─ReflectiveTactics.unify_abstract_ 5.2% 7.3% 1 0.292s │ └unify (constr) (constr) --------- 2.1% 2.1% 1 0.084s └─Glue.refine_to_reflective_glue' ----- 0.0% 11.1% 1 0.440s ├─Glue.zrange_to_reflective --------- 0.0% 7.1% 1 0.284s │└Glue.zrange_to_reflective_goal ---- 4.3% 5.5% 1 0.220s └─Glue.split_BoundedWordToZ --------- 0.1% 2.0% 1 0.080s Finished transaction in 7.078 secs (6.728u,0.s) (successful) Closed under the global context total time: 3.976s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 99.0% 1 3.936s ─ReflectiveTactics.do_reflective_pipelin 0.0% 87.9% 1 3.496s ─ReflectiveTactics.solve_side_conditions 0.0% 86.9% 1 3.456s ─ReflectiveTactics.do_reify ------------ 0.0% 56.9% 1 2.264s ─Reify.Reify_rhs_gen ------------------- 1.8% 56.2% 1 2.236s ─Reify.do_reify_abs_goal --------------- 36.1% 36.5% 2 1.452s ─Reify.do_reifyf_goal ------------------ 34.8% 35.1% 29 1.396s ─ReflectiveTactics.solve_post_reified_si 0.6% 30.0% 1 1.192s ─UnifyAbstractReflexivity.unify_transfor 17.7% 21.7% 7 0.240s ─Glue.refine_to_reflective_glue' ------- 0.0% 11.1% 1 0.440s ─eexact -------------------------------- 10.9% 10.9% 31 0.024s ─ReflectiveTactics.unify_abstract_cbv_in 5.2% 7.3% 1 0.292s ─Glue.zrange_to_reflective ------------- 0.0% 7.1% 1 0.284s ─prove_interp_compile_correct ---------- 0.0% 5.7% 1 0.228s ─Glue.zrange_to_reflective_goal -------- 4.3% 5.5% 1 0.220s ─unify (constr) (constr) --------------- 5.3% 5.3% 6 0.084s ─rewrite ?EtaInterp.InterpExprEta ------ 5.2% 5.2% 1 0.208s ─rewrite H ----------------------------- 3.5% 3.5% 1 0.140s ─tac ----------------------------------- 1.9% 2.6% 2 0.104s ─reflexivity --------------------------- 2.2% 2.2% 7 0.028s ─Reify.transitivity_tt ----------------- 0.0% 2.2% 2 0.056s ─transitivity -------------------------- 2.0% 2.0% 5 0.048s ─Glue.split_BoundedWordToZ ------------- 0.1% 2.0% 1 0.080s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 99.0% 1 3.936s ├─ReflectiveTactics.do_reflective_pipel 0.0% 87.9% 1 3.496s │└ReflectiveTactics.solve_side_conditio 0.0% 86.9% 1 3.456s │ ├─ReflectiveTactics.do_reify -------- 0.0% 56.9% 1 2.264s │ │└Reify.Reify_rhs_gen --------------- 1.8% 56.2% 1 2.236s │ │ ├─Reify.do_reify_abs_goal --------- 36.1% 36.5% 2 1.452s │ │ │└Reify.do_reifyf_goal ------------ 34.8% 35.1% 29 1.396s │ │ │└eexact -------------------------- 10.1% 10.1% 29 0.024s │ │ ├─prove_interp_compile_correct ---- 0.0% 5.7% 1 0.228s │ │ │└rewrite ?EtaInterp.InterpExprEta 5.2% 5.2% 1 0.208s │ │ ├─rewrite H ----------------------- 3.5% 3.5% 1 0.140s │ │ ├─tac ----------------------------- 1.9% 2.6% 1 0.104s │ │ └─Reify.transitivity_tt ----------- 0.0% 2.2% 2 0.056s │ │ └transitivity -------------------- 2.0% 2.0% 4 0.048s │ └─ReflectiveTactics.solve_post_reifie 0.6% 30.0% 1 1.192s │ ├─UnifyAbstractReflexivity.unify_tr 17.7% 21.7% 7 0.240s │ │└unify (constr) (constr) --------- 3.2% 3.2% 5 0.048s │ └─ReflectiveTactics.unify_abstract_ 5.2% 7.3% 1 0.292s │ └unify (constr) (constr) --------- 2.1% 2.1% 1 0.084s └─Glue.refine_to_reflective_glue' ----- 0.0% 11.1% 1 0.440s ├─Glue.zrange_to_reflective --------- 0.0% 7.1% 1 0.284s │└Glue.zrange_to_reflective_goal ---- 4.3% 5.5% 1 0.220s └─Glue.split_BoundedWordToZ --------- 0.1% 2.0% 1 0.080s src/Specific/X25519/C64/fecarry (real: 27.11, user: 24.99, sys: 0.21, mem: 786052 ko) COQC src/Specific/solinas32_2e255m765_12limbs/Synthesis.v src/Specific/solinas32_2e255m765_12limbs/Synthesis (real: 40.13, user: 36.92, sys: 0.26, mem: 728464 ko) COQC src/Specific/solinas32_2e255m765_13limbs/Synthesis.v src/Specific/solinas32_2e255m765_13limbs/Synthesis (real: 49.44, user: 45.75, sys: 0.18, mem: 744240 ko) COQC src/Specific/X25519/C64/femul.v Finished transaction in 8.415 secs (7.664u,0.015s) (successful) total time: 7.616s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.8% 1 7.220s ─ReflectiveTactics.do_reflective_pipelin 0.0% 85.0% 1 6.476s ─ReflectiveTactics.solve_side_conditions 0.0% 84.2% 1 6.416s ─ReflectiveTactics.do_reify ------------ 0.0% 50.3% 1 3.832s ─Reify.Reify_rhs_gen ------------------- 1.8% 49.4% 1 3.760s ─ReflectiveTactics.solve_post_reified_si 0.5% 33.9% 1 2.584s ─Reify.do_reify_abs_goal --------------- 31.1% 31.4% 2 2.392s ─Reify.do_reifyf_goal ------------------ 30.0% 30.3% 58 1.528s ─UnifyAbstractReflexivity.unify_transfor 22.1% 27.3% 7 0.600s ─Glue.refine_to_reflective_glue' ------- 0.0% 9.8% 1 0.744s ─eexact -------------------------------- 8.2% 8.2% 60 0.024s ─Glue.zrange_to_reflective ------------- 0.1% 6.8% 1 0.516s ─unify (constr) (constr) --------------- 5.9% 5.9% 6 0.124s ─prove_interp_compile_correct ---------- 0.0% 5.8% 1 0.444s ─ReflectiveTactics.unify_abstract_cbv_in 3.9% 5.7% 1 0.432s ─rewrite ?EtaInterp.InterpExprEta ------ 5.4% 5.4% 1 0.408s ─synthesize ---------------------------- 0.0% 5.2% 1 0.396s ─Glue.zrange_to_reflective_goal -------- 3.0% 5.0% 1 0.384s ─IntegrationTestTemporaryMiscCommon.do_r 0.1% 4.8% 1 0.364s ─change G' ----------------------------- 3.9% 3.9% 1 0.300s ─rewrite H ----------------------------- 3.0% 3.0% 1 0.232s ─tac ----------------------------------- 1.5% 2.3% 2 0.176s ─Reify.transitivity_tt ----------------- 0.0% 2.1% 2 0.092s ─reflexivity --------------------------- 2.0% 2.0% 7 0.052s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.8% 1 7.220s ├─ReflectiveTactics.do_reflective_pipel 0.0% 85.0% 1 6.476s │└ReflectiveTactics.solve_side_conditio 0.0% 84.2% 1 6.416s │ ├─ReflectiveTactics.do_reify -------- 0.0% 50.3% 1 3.832s │ │└Reify.Reify_rhs_gen --------------- 1.8% 49.4% 1 3.760s │ │ ├─Reify.do_reify_abs_goal --------- 31.1% 31.4% 2 2.392s │ │ │└Reify.do_reifyf_goal ------------ 30.0% 30.3% 58 1.528s │ │ │└eexact -------------------------- 7.6% 7.6% 58 0.020s │ │ ├─prove_interp_compile_correct ---- 0.0% 5.8% 1 0.444s │ │ │└rewrite ?EtaInterp.InterpExprEta 5.4% 5.4% 1 0.408s │ │ ├─rewrite H ----------------------- 3.0% 3.0% 1 0.232s │ │ ├─tac ----------------------------- 1.5% 2.3% 1 0.176s │ │ └─Reify.transitivity_tt ----------- 0.0% 2.1% 2 0.092s │ └─ReflectiveTactics.solve_post_reifie 0.5% 33.9% 1 2.584s │ ├─UnifyAbstractReflexivity.unify_tr 22.1% 27.3% 7 0.600s │ │└unify (constr) (constr) --------- 4.3% 4.3% 5 0.096s │ └─ReflectiveTactics.unify_abstract_ 3.9% 5.7% 1 0.432s └─Glue.refine_to_reflective_glue' ----- 0.0% 9.8% 1 0.744s └Glue.zrange_to_reflective ----------- 0.1% 6.8% 1 0.516s └Glue.zrange_to_reflective_goal ------ 3.0% 5.0% 1 0.384s ─synthesize ---------------------------- 0.0% 5.2% 1 0.396s └IntegrationTestTemporaryMiscCommon.do_r 0.1% 4.8% 1 0.364s └change G' ----------------------------- 3.9% 3.9% 1 0.300s Finished transaction in 14.616 secs (13.528u,0.008s) (successful) Closed under the global context total time: 7.616s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.8% 1 7.220s ─ReflectiveTactics.do_reflective_pipelin 0.0% 85.0% 1 6.476s ─ReflectiveTactics.solve_side_conditions 0.0% 84.2% 1 6.416s ─ReflectiveTactics.do_reify ------------ 0.0% 50.3% 1 3.832s ─Reify.Reify_rhs_gen ------------------- 1.8% 49.4% 1 3.760s ─ReflectiveTactics.solve_post_reified_si 0.5% 33.9% 1 2.584s ─Reify.do_reify_abs_goal --------------- 31.1% 31.4% 2 2.392s ─Reify.do_reifyf_goal ------------------ 30.0% 30.3% 58 1.528s ─UnifyAbstractReflexivity.unify_transfor 22.1% 27.3% 7 0.600s ─Glue.refine_to_reflective_glue' ------- 0.0% 9.8% 1 0.744s ─eexact -------------------------------- 8.2% 8.2% 60 0.024s ─Glue.zrange_to_reflective ------------- 0.1% 6.8% 1 0.516s ─unify (constr) (constr) --------------- 5.9% 5.9% 6 0.124s ─prove_interp_compile_correct ---------- 0.0% 5.8% 1 0.444s ─ReflectiveTactics.unify_abstract_cbv_in 3.9% 5.7% 1 0.432s ─rewrite ?EtaInterp.InterpExprEta ------ 5.4% 5.4% 1 0.408s ─synthesize ---------------------------- 0.0% 5.2% 1 0.396s ─Glue.zrange_to_reflective_goal -------- 3.0% 5.0% 1 0.384s ─IntegrationTestTemporaryMiscCommon.do_r 0.1% 4.8% 1 0.364s ─change G' ----------------------------- 3.9% 3.9% 1 0.300s ─rewrite H ----------------------------- 3.0% 3.0% 1 0.232s ─tac ----------------------------------- 1.5% 2.3% 2 0.176s ─Reify.transitivity_tt ----------------- 0.0% 2.1% 2 0.092s ─reflexivity --------------------------- 2.0% 2.0% 7 0.052s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.8% 1 7.220s ├─ReflectiveTactics.do_reflective_pipel 0.0% 85.0% 1 6.476s │└ReflectiveTactics.solve_side_conditio 0.0% 84.2% 1 6.416s │ ├─ReflectiveTactics.do_reify -------- 0.0% 50.3% 1 3.832s │ │└Reify.Reify_rhs_gen --------------- 1.8% 49.4% 1 3.760s │ │ ├─Reify.do_reify_abs_goal --------- 31.1% 31.4% 2 2.392s │ │ │└Reify.do_reifyf_goal ------------ 30.0% 30.3% 58 1.528s │ │ │└eexact -------------------------- 7.6% 7.6% 58 0.020s │ │ ├─prove_interp_compile_correct ---- 0.0% 5.8% 1 0.444s │ │ │└rewrite ?EtaInterp.InterpExprEta 5.4% 5.4% 1 0.408s │ │ ├─rewrite H ----------------------- 3.0% 3.0% 1 0.232s │ │ ├─tac ----------------------------- 1.5% 2.3% 1 0.176s │ │ └─Reify.transitivity_tt ----------- 0.0% 2.1% 2 0.092s │ └─ReflectiveTactics.solve_post_reifie 0.5% 33.9% 1 2.584s │ ├─UnifyAbstractReflexivity.unify_tr 22.1% 27.3% 7 0.600s │ │└unify (constr) (constr) --------- 4.3% 4.3% 5 0.096s │ └─ReflectiveTactics.unify_abstract_ 3.9% 5.7% 1 0.432s └─Glue.refine_to_reflective_glue' ----- 0.0% 9.8% 1 0.744s └Glue.zrange_to_reflective ----------- 0.1% 6.8% 1 0.516s └Glue.zrange_to_reflective_goal ------ 3.0% 5.0% 1 0.384s ─synthesize ---------------------------- 0.0% 5.2% 1 0.396s └IntegrationTestTemporaryMiscCommon.do_r 0.1% 4.8% 1 0.364s └change G' ----------------------------- 3.9% 3.9% 1 0.300s src/Specific/X25519/C64/femul (real: 39.72, user: 36.32, sys: 0.26, mem: 825448 ko) COQC src/Specific/X25519/C64/feaddDisplay > src/Specific/X25519/C64/feaddDisplay.log COQC src/Specific/X25519/C64/fecarryDisplay > src/Specific/X25519/C64/fecarryDisplay.log COQC src/Specific/X25519/C64/fesub.v Finished transaction in 3.513 secs (3.211u,0.s) (successful) total time: 3.164s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.6% 1 3.088s ─ReflectiveTactics.do_reflective_pipelin 0.0% 74.1% 1 2.344s ─ReflectiveTactics.solve_side_conditions 0.0% 72.9% 1 2.308s ─ReflectiveTactics.do_reify ------------ 0.0% 38.6% 1 1.220s ─Reify.Reify_rhs_gen ------------------- 1.5% 37.2% 1 1.176s ─ReflectiveTactics.solve_post_reified_si 0.9% 34.4% 1 1.088s ─UnifyAbstractReflexivity.unify_transfor 19.2% 23.9% 7 0.204s ─Glue.refine_to_reflective_glue' ------- 0.0% 23.5% 1 0.744s ─Reify.do_reify_abs_goal --------------- 19.2% 19.5% 2 0.616s ─Reify.do_reifyf_goal ------------------ 18.0% 18.3% 16 0.580s ─Glue.zrange_to_reflective ------------- 0.1% 15.4% 1 0.488s ─Glue.zrange_to_reflective_goal -------- 6.8% 11.5% 1 0.364s ─ReflectiveTactics.unify_abstract_cbv_in 6.2% 9.0% 1 0.284s ─unify (constr) (constr) --------------- 5.9% 5.9% 6 0.080s ─Glue.pattern_sig_sig_assoc ------------ 0.0% 4.6% 1 0.144s ─eexact -------------------------------- 4.4% 4.4% 18 0.012s ─Glue.pattern_proj1_sig_in_sig --------- 1.4% 4.3% 1 0.136s ─prove_interp_compile_correct ---------- 0.0% 3.9% 1 0.124s ─rewrite H ----------------------------- 3.8% 3.8% 1 0.120s ─assert (H : is_bounded_by' bounds (map' 3.8% 3.8% 2 0.064s ─rewrite ?EtaInterp.InterpExprEta ------ 3.5% 3.5% 1 0.112s ─pose proof (pf : Interpretation.Bo 2.9% 2.9% 1 0.092s ─Glue.split_BoundedWordToZ ------------- 0.1% 2.8% 1 0.088s ─tac ----------------------------------- 1.9% 2.5% 2 0.080s ─reflexivity --------------------------- 2.4% 2.4% 7 0.028s ─synthesize ---------------------------- 0.0% 2.4% 1 0.076s ─destruct_sig -------------------------- 0.0% 2.4% 4 0.040s ─destruct x ---------------------------- 2.4% 2.4% 4 0.032s ─clearbody (ne_var_list) --------------- 2.3% 2.3% 4 0.060s ─Reify.transitivity_tt ----------------- 0.1% 2.3% 2 0.036s ─transitivity -------------------------- 2.1% 2.1% 5 0.032s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.6% 1 3.088s ├─ReflectiveTactics.do_reflective_pipel 0.0% 74.1% 1 2.344s │└ReflectiveTactics.solve_side_conditio 0.0% 72.9% 1 2.308s │ ├─ReflectiveTactics.do_reify -------- 0.0% 38.6% 1 1.220s │ │└Reify.Reify_rhs_gen --------------- 1.5% 37.2% 1 1.176s │ │ ├─Reify.do_reify_abs_goal --------- 19.2% 19.5% 2 0.616s │ │ │└Reify.do_reifyf_goal ------------ 18.0% 18.3% 16 0.580s │ │ │└eexact -------------------------- 3.9% 3.9% 16 0.012s │ │ ├─prove_interp_compile_correct ---- 0.0% 3.9% 1 0.124s │ │ │└rewrite ?EtaInterp.InterpExprEta 3.5% 3.5% 1 0.112s │ │ ├─rewrite H ----------------------- 3.8% 3.8% 1 0.120s │ │ ├─tac ----------------------------- 1.9% 2.5% 1 0.080s │ │ └─Reify.transitivity_tt ----------- 0.1% 2.3% 2 0.036s │ │ └transitivity -------------------- 2.0% 2.0% 4 0.032s │ └─ReflectiveTactics.solve_post_reifie 0.9% 34.4% 1 1.088s │ ├─UnifyAbstractReflexivity.unify_tr 19.2% 23.9% 7 0.204s │ │└unify (constr) (constr) --------- 3.4% 3.4% 5 0.036s │ └─ReflectiveTactics.unify_abstract_ 6.2% 9.0% 1 0.284s │ └unify (constr) (constr) --------- 2.5% 2.5% 1 0.080s └─Glue.refine_to_reflective_glue' ----- 0.0% 23.5% 1 0.744s ├─Glue.zrange_to_reflective --------- 0.1% 15.4% 1 0.488s │ ├─Glue.zrange_to_reflective_goal -- 6.8% 11.5% 1 0.364s │ │└pose proof (pf : Interpretat 2.9% 2.9% 1 0.092s │ └─assert (H : is_bounded_by' bounds 3.8% 3.8% 2 0.064s ├─Glue.pattern_sig_sig_assoc -------- 0.0% 4.6% 1 0.144s │└Glue.pattern_proj1_sig_in_sig ----- 1.4% 4.3% 1 0.136s └─Glue.split_BoundedWordToZ --------- 0.1% 2.8% 1 0.088s └destruct_sig ---------------------- 0.0% 2.4% 4 0.040s ─synthesize ---------------------------- 0.0% 2.4% 1 0.076s Finished transaction in 6.12 secs (5.64u,0.008s) (successful) Closed under the global context total time: 3.164s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.6% 1 3.088s ─ReflectiveTactics.do_reflective_pipelin 0.0% 74.1% 1 2.344s ─ReflectiveTactics.solve_side_conditions 0.0% 72.9% 1 2.308s ─ReflectiveTactics.do_reify ------------ 0.0% 38.6% 1 1.220s ─Reify.Reify_rhs_gen ------------------- 1.5% 37.2% 1 1.176s ─ReflectiveTactics.solve_post_reified_si 0.9% 34.4% 1 1.088s ─UnifyAbstractReflexivity.unify_transfor 19.2% 23.9% 7 0.204s ─Glue.refine_to_reflective_glue' ------- 0.0% 23.5% 1 0.744s ─Reify.do_reify_abs_goal --------------- 19.2% 19.5% 2 0.616s ─Reify.do_reifyf_goal ------------------ 18.0% 18.3% 16 0.580s ─Glue.zrange_to_reflective ------------- 0.1% 15.4% 1 0.488s ─Glue.zrange_to_reflective_goal -------- 6.8% 11.5% 1 0.364s ─ReflectiveTactics.unify_abstract_cbv_in 6.2% 9.0% 1 0.284s ─unify (constr) (constr) --------------- 5.9% 5.9% 6 0.080s ─Glue.pattern_sig_sig_assoc ------------ 0.0% 4.6% 1 0.144s ─eexact -------------------------------- 4.4% 4.4% 18 0.012s ─Glue.pattern_proj1_sig_in_sig --------- 1.4% 4.3% 1 0.136s ─prove_interp_compile_correct ---------- 0.0% 3.9% 1 0.124s ─rewrite H ----------------------------- 3.8% 3.8% 1 0.120s ─assert (H : is_bounded_by' bounds (map' 3.8% 3.8% 2 0.064s ─rewrite ?EtaInterp.InterpExprEta ------ 3.5% 3.5% 1 0.112s ─pose proof (pf : Interpretation.Bo 2.9% 2.9% 1 0.092s ─Glue.split_BoundedWordToZ ------------- 0.1% 2.8% 1 0.088s ─tac ----------------------------------- 1.9% 2.5% 2 0.080s ─reflexivity --------------------------- 2.4% 2.4% 7 0.028s ─synthesize ---------------------------- 0.0% 2.4% 1 0.076s ─destruct_sig -------------------------- 0.0% 2.4% 4 0.040s ─destruct x ---------------------------- 2.4% 2.4% 4 0.032s ─clearbody (ne_var_list) --------------- 2.3% 2.3% 4 0.060s ─Reify.transitivity_tt ----------------- 0.1% 2.3% 2 0.036s ─transitivity -------------------------- 2.1% 2.1% 5 0.032s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.6% 1 3.088s ├─ReflectiveTactics.do_reflective_pipel 0.0% 74.1% 1 2.344s │└ReflectiveTactics.solve_side_conditio 0.0% 72.9% 1 2.308s │ ├─ReflectiveTactics.do_reify -------- 0.0% 38.6% 1 1.220s │ │└Reify.Reify_rhs_gen --------------- 1.5% 37.2% 1 1.176s │ │ ├─Reify.do_reify_abs_goal --------- 19.2% 19.5% 2 0.616s │ │ │└Reify.do_reifyf_goal ------------ 18.0% 18.3% 16 0.580s │ │ │└eexact -------------------------- 3.9% 3.9% 16 0.012s │ │ ├─prove_interp_compile_correct ---- 0.0% 3.9% 1 0.124s │ │ │└rewrite ?EtaInterp.InterpExprEta 3.5% 3.5% 1 0.112s │ │ ├─rewrite H ----------------------- 3.8% 3.8% 1 0.120s │ │ ├─tac ----------------------------- 1.9% 2.5% 1 0.080s │ │ └─Reify.transitivity_tt ----------- 0.1% 2.3% 2 0.036s │ │ └transitivity -------------------- 2.0% 2.0% 4 0.032s │ └─ReflectiveTactics.solve_post_reifie 0.9% 34.4% 1 1.088s │ ├─UnifyAbstractReflexivity.unify_tr 19.2% 23.9% 7 0.204s │ │└unify (constr) (constr) --------- 3.4% 3.4% 5 0.036s │ └─ReflectiveTactics.unify_abstract_ 6.2% 9.0% 1 0.284s │ └unify (constr) (constr) --------- 2.5% 2.5% 1 0.080s └─Glue.refine_to_reflective_glue' ----- 0.0% 23.5% 1 0.744s ├─Glue.zrange_to_reflective --------- 0.1% 15.4% 1 0.488s │ ├─Glue.zrange_to_reflective_goal -- 6.8% 11.5% 1 0.364s │ │└pose proof (pf : Interpretat 2.9% 2.9% 1 0.092s │ └─assert (H : is_bounded_by' bounds 3.8% 3.8% 2 0.064s ├─Glue.pattern_sig_sig_assoc -------- 0.0% 4.6% 1 0.144s │└Glue.pattern_proj1_sig_in_sig ----- 1.4% 4.3% 1 0.136s └─Glue.split_BoundedWordToZ --------- 0.1% 2.8% 1 0.088s └destruct_sig ---------------------- 0.0% 2.4% 4 0.040s ─synthesize ---------------------------- 0.0% 2.4% 1 0.076s src/Specific/X25519/C64/fesub (real: 24.71, user: 22.65, sys: 0.24, mem: 778792 ko) COQC src/Specific/X25519/C64/fesquare.v Finished transaction in 6.132 secs (5.516u,0.012s) (successful) total time: 5.480s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize ---------------------------- -0.0% 100.0% 1 5.480s ─Pipeline.refine_reflectively_gen ------ 0.0% 95.7% 1 5.244s ─ReflectiveTactics.do_reflective_pipelin 0.0% 88.6% 1 4.856s ─ReflectiveTactics.solve_side_conditions 0.0% 87.7% 1 4.804s ─ReflectiveTactics.do_reify ------------ 0.0% 53.3% 1 2.920s ─Reify.Reify_rhs_gen ------------------- 2.0% 52.5% 1 2.876s ─ReflectiveTactics.solve_post_reified_si 0.6% 34.4% 1 1.884s ─Reify.do_reify_abs_goal --------------- 33.2% 33.6% 2 1.844s ─Reify.do_reifyf_goal ------------------ 31.5% 32.0% 47 1.392s ─UnifyAbstractReflexivity.unify_transfor 21.9% 26.6% 7 0.400s ─eexact -------------------------------- 10.0% 10.0% 49 0.028s ─Glue.refine_to_reflective_glue' ------- 0.0% 7.1% 1 0.388s ─ReflectiveTactics.unify_abstract_cbv_in 5.0% 6.9% 1 0.380s ─unify (constr) (constr) --------------- 5.8% 5.8% 6 0.104s ─prove_interp_compile_correct ---------- 0.0% 5.8% 1 0.316s ─rewrite ?EtaInterp.InterpExprEta ------ 5.3% 5.3% 1 0.288s ─Glue.zrange_to_reflective ------------- 0.1% 5.1% 1 0.280s ─IntegrationTestTemporaryMiscCommon.do_r 0.1% 4.0% 1 0.220s ─Glue.zrange_to_reflective_goal -------- 3.1% 3.9% 1 0.212s ─change G' ----------------------------- 3.4% 3.4% 1 0.184s ─tac ----------------------------------- 2.0% 2.8% 2 0.156s ─rewrite H ----------------------------- 2.8% 2.8% 1 0.156s ─reflexivity --------------------------- 2.8% 2.8% 7 0.064s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize ---------------------------- -0.0% 100.0% 1 5.480s ├─Pipeline.refine_reflectively_gen ---- 0.0% 95.7% 1 5.244s │ ├─ReflectiveTactics.do_reflective_pip 0.0% 88.6% 1 4.856s │ │└ReflectiveTactics.solve_side_condit 0.0% 87.7% 1 4.804s │ │ ├─ReflectiveTactics.do_reify ------ 0.0% 53.3% 1 2.920s │ │ │└Reify.Reify_rhs_gen ------------- 2.0% 52.5% 1 2.876s │ │ │ ├─Reify.do_reify_abs_goal ------- 33.2% 33.6% 2 1.844s │ │ │ │└Reify.do_reifyf_goal ---------- 31.5% 32.0% 47 1.392s │ │ │ │└eexact ------------------------ 9.1% 9.1% 47 0.024s │ │ │ ├─prove_interp_compile_correct -- 0.0% 5.8% 1 0.316s │ │ │ │└rewrite ?EtaInterp.InterpExprEt 5.3% 5.3% 1 0.288s │ │ │ ├─tac --------------------------- 2.0% 2.8% 1 0.156s │ │ │ └─rewrite H --------------------- 2.8% 2.8% 1 0.156s │ │ └─ReflectiveTactics.solve_post_reif 0.6% 34.4% 1 1.884s │ │ ├─UnifyAbstractReflexivity.unify_ 21.9% 26.6% 7 0.400s │ │ │└unify (constr) (constr) ------- 3.9% 3.9% 5 0.072s │ │ └─ReflectiveTactics.unify_abstrac 5.0% 6.9% 1 0.380s │ └─Glue.refine_to_reflective_glue' --- 0.0% 7.1% 1 0.388s │ └Glue.zrange_to_reflective --------- 0.1% 5.1% 1 0.280s │ └Glue.zrange_to_reflective_goal ---- 3.1% 3.9% 1 0.212s └─IntegrationTestTemporaryMiscCommon.do 0.1% 4.0% 1 0.220s └change G' --------------------------- 3.4% 3.4% 1 0.184s Finished transaction in 10.475 secs (9.728u,0.007s) (successful) Closed under the global context total time: 5.480s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize ---------------------------- -0.0% 100.0% 1 5.480s ─Pipeline.refine_reflectively_gen ------ 0.0% 95.7% 1 5.244s ─ReflectiveTactics.do_reflective_pipelin 0.0% 88.6% 1 4.856s ─ReflectiveTactics.solve_side_conditions 0.0% 87.7% 1 4.804s ─ReflectiveTactics.do_reify ------------ 0.0% 53.3% 1 2.920s ─Reify.Reify_rhs_gen ------------------- 2.0% 52.5% 1 2.876s ─ReflectiveTactics.solve_post_reified_si 0.6% 34.4% 1 1.884s ─Reify.do_reify_abs_goal --------------- 33.2% 33.6% 2 1.844s ─Reify.do_reifyf_goal ------------------ 31.5% 32.0% 47 1.392s ─UnifyAbstractReflexivity.unify_transfor 21.9% 26.6% 7 0.400s ─eexact -------------------------------- 10.0% 10.0% 49 0.028s ─Glue.refine_to_reflective_glue' ------- 0.0% 7.1% 1 0.388s ─ReflectiveTactics.unify_abstract_cbv_in 5.0% 6.9% 1 0.380s ─unify (constr) (constr) --------------- 5.8% 5.8% 6 0.104s ─prove_interp_compile_correct ---------- 0.0% 5.8% 1 0.316s ─rewrite ?EtaInterp.InterpExprEta ------ 5.3% 5.3% 1 0.288s ─Glue.zrange_to_reflective ------------- 0.1% 5.1% 1 0.280s ─IntegrationTestTemporaryMiscCommon.do_r 0.1% 4.0% 1 0.220s ─Glue.zrange_to_reflective_goal -------- 3.1% 3.9% 1 0.212s ─change G' ----------------------------- 3.4% 3.4% 1 0.184s ─tac ----------------------------------- 2.0% 2.8% 2 0.156s ─rewrite H ----------------------------- 2.8% 2.8% 1 0.156s ─reflexivity --------------------------- 2.8% 2.8% 7 0.064s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize ---------------------------- -0.0% 100.0% 1 5.480s ├─Pipeline.refine_reflectively_gen ---- 0.0% 95.7% 1 5.244s │ ├─ReflectiveTactics.do_reflective_pip 0.0% 88.6% 1 4.856s │ │└ReflectiveTactics.solve_side_condit 0.0% 87.7% 1 4.804s │ │ ├─ReflectiveTactics.do_reify ------ 0.0% 53.3% 1 2.920s │ │ │└Reify.Reify_rhs_gen ------------- 2.0% 52.5% 1 2.876s │ │ │ ├─Reify.do_reify_abs_goal ------- 33.2% 33.6% 2 1.844s │ │ │ │└Reify.do_reifyf_goal ---------- 31.5% 32.0% 47 1.392s │ │ │ │└eexact ------------------------ 9.1% 9.1% 47 0.024s │ │ │ ├─prove_interp_compile_correct -- 0.0% 5.8% 1 0.316s │ │ │ │└rewrite ?EtaInterp.InterpExprEt 5.3% 5.3% 1 0.288s │ │ │ ├─tac --------------------------- 2.0% 2.8% 1 0.156s │ │ │ └─rewrite H --------------------- 2.8% 2.8% 1 0.156s │ │ └─ReflectiveTactics.solve_post_reif 0.6% 34.4% 1 1.884s │ │ ├─UnifyAbstractReflexivity.unify_ 21.9% 26.6% 7 0.400s │ │ │└unify (constr) (constr) ------- 3.9% 3.9% 5 0.072s │ │ └─ReflectiveTactics.unify_abstrac 5.0% 6.9% 1 0.380s │ └─Glue.refine_to_reflective_glue' --- 0.0% 7.1% 1 0.388s │ └Glue.zrange_to_reflective --------- 0.1% 5.1% 1 0.280s │ └Glue.zrange_to_reflective_goal ---- 3.1% 3.9% 1 0.212s └─IntegrationTestTemporaryMiscCommon.do 0.1% 4.0% 1 0.220s └change G' --------------------------- 3.4% 3.4% 1 0.184s src/Specific/X25519/C64/fesquare (real: 33.08, user: 30.13, sys: 0.24, mem: 799620 ko) COQC src/Specific/X25519/C64/femulDisplay > src/Specific/X25519/C64/femulDisplay.log COQC src/Specific/X25519/C64/freeze.v Finished transaction in 7.307 secs (6.763u,0.011s) (successful) total time: 6.732s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_freeze --------------------- 0.0% 100.0% 1 6.732s ─Pipeline.refine_reflectively_gen ------ 0.0% 99.3% 1 6.684s ─ReflectiveTactics.do_reflective_pipelin 0.0% 92.8% 1 6.248s ─ReflectiveTactics.solve_side_conditions 0.0% 92.0% 1 6.192s ─ReflectiveTactics.do_reify ------------ -0.0% 60.3% 1 4.060s ─Reify.Reify_rhs_gen ------------------- 1.5% 59.6% 1 4.012s ─Reify.do_reify_abs_goal --------------- 42.4% 42.7% 2 2.876s ─Reify.do_reifyf_goal ------------------ 41.3% 41.7% 129 2.804s ─ReflectiveTactics.solve_post_reified_si 0.6% 31.7% 1 2.132s ─UnifyAbstractReflexivity.unify_transfor 21.7% 25.8% 7 0.424s ─eexact -------------------------------- 13.7% 13.7% 131 0.036s ─Glue.refine_to_reflective_glue' ------- 0.0% 6.5% 1 0.436s ─prove_interp_compile_correct ---------- 0.0% 5.1% 1 0.344s ─ReflectiveTactics.unify_abstract_cbv_in 3.4% 5.0% 1 0.336s ─rewrite ?EtaInterp.InterpExprEta ------ 4.7% 4.7% 1 0.316s ─unify (constr) (constr) --------------- 4.6% 4.6% 6 0.100s ─Glue.zrange_to_reflective ------------- 0.0% 4.2% 1 0.280s ─Glue.zrange_to_reflective_goal -------- 2.4% 3.3% 1 0.220s ─Reify.transitivity_tt ----------------- 0.1% 2.6% 2 0.116s ─rewrite H ----------------------------- 2.6% 2.6% 1 0.172s ─tac ----------------------------------- 1.5% 2.3% 2 0.156s ─reflexivity --------------------------- 2.3% 2.3% 7 0.052s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_freeze --------------------- 0.0% 100.0% 1 6.732s └Pipeline.refine_reflectively_gen ------ 0.0% 99.3% 1 6.684s ├─ReflectiveTactics.do_reflective_pipel 0.0% 92.8% 1 6.248s │└ReflectiveTactics.solve_side_conditio 0.0% 92.0% 1 6.192s │ ├─ReflectiveTactics.do_reify -------- -0.0% 60.3% 1 4.060s │ │└Reify.Reify_rhs_gen --------------- 1.5% 59.6% 1 4.012s │ │ ├─Reify.do_reify_abs_goal --------- 42.4% 42.7% 2 2.876s │ │ │└Reify.do_reifyf_goal ------------ 41.3% 41.7% 129 2.804s │ │ │└eexact -------------------------- 13.0% 13.0% 129 0.036s │ │ ├─prove_interp_compile_correct ---- 0.0% 5.1% 1 0.344s │ │ │└rewrite ?EtaInterp.InterpExprEta 4.7% 4.7% 1 0.316s │ │ ├─Reify.transitivity_tt ----------- 0.1% 2.6% 2 0.116s │ │ ├─rewrite H ----------------------- 2.6% 2.6% 1 0.172s │ │ └─tac ----------------------------- 1.5% 2.3% 1 0.156s │ └─ReflectiveTactics.solve_post_reifie 0.6% 31.7% 1 2.132s │ ├─UnifyAbstractReflexivity.unify_tr 21.7% 25.8% 7 0.424s │ │└unify (constr) (constr) --------- 3.1% 3.1% 5 0.084s │ └─ReflectiveTactics.unify_abstract_ 3.4% 5.0% 1 0.336s └─Glue.refine_to_reflective_glue' ----- 0.0% 6.5% 1 0.436s └Glue.zrange_to_reflective ----------- 0.0% 4.2% 1 0.280s └Glue.zrange_to_reflective_goal ------ 2.4% 3.3% 1 0.220s Finished transaction in 10.495 secs (9.756u,0.s) (successful) Closed under the global context total time: 6.732s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_freeze --------------------- 0.0% 100.0% 1 6.732s ─Pipeline.refine_reflectively_gen ------ 0.0% 99.3% 1 6.684s ─ReflectiveTactics.do_reflective_pipelin 0.0% 92.8% 1 6.248s ─ReflectiveTactics.solve_side_conditions 0.0% 92.0% 1 6.192s ─ReflectiveTactics.do_reify ------------ -0.0% 60.3% 1 4.060s ─Reify.Reify_rhs_gen ------------------- 1.5% 59.6% 1 4.012s ─Reify.do_reify_abs_goal --------------- 42.4% 42.7% 2 2.876s ─Reify.do_reifyf_goal ------------------ 41.3% 41.7% 129 2.804s ─ReflectiveTactics.solve_post_reified_si 0.6% 31.7% 1 2.132s ─UnifyAbstractReflexivity.unify_transfor 21.7% 25.8% 7 0.424s ─eexact -------------------------------- 13.7% 13.7% 131 0.036s ─Glue.refine_to_reflective_glue' ------- 0.0% 6.5% 1 0.436s ─prove_interp_compile_correct ---------- 0.0% 5.1% 1 0.344s ─ReflectiveTactics.unify_abstract_cbv_in 3.4% 5.0% 1 0.336s ─rewrite ?EtaInterp.InterpExprEta ------ 4.7% 4.7% 1 0.316s ─unify (constr) (constr) --------------- 4.6% 4.6% 6 0.100s ─Glue.zrange_to_reflective ------------- 0.0% 4.2% 1 0.280s ─Glue.zrange_to_reflective_goal -------- 2.4% 3.3% 1 0.220s ─Reify.transitivity_tt ----------------- 0.1% 2.6% 2 0.116s ─rewrite H ----------------------------- 2.6% 2.6% 1 0.172s ─tac ----------------------------------- 1.5% 2.3% 2 0.156s ─reflexivity --------------------------- 2.3% 2.3% 7 0.052s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_freeze --------------------- 0.0% 100.0% 1 6.732s └Pipeline.refine_reflectively_gen ------ 0.0% 99.3% 1 6.684s ├─ReflectiveTactics.do_reflective_pipel 0.0% 92.8% 1 6.248s │└ReflectiveTactics.solve_side_conditio 0.0% 92.0% 1 6.192s │ ├─ReflectiveTactics.do_reify -------- -0.0% 60.3% 1 4.060s │ │└Reify.Reify_rhs_gen --------------- 1.5% 59.6% 1 4.012s │ │ ├─Reify.do_reify_abs_goal --------- 42.4% 42.7% 2 2.876s │ │ │└Reify.do_reifyf_goal ------------ 41.3% 41.7% 129 2.804s │ │ │└eexact -------------------------- 13.0% 13.0% 129 0.036s │ │ ├─prove_interp_compile_correct ---- 0.0% 5.1% 1 0.344s │ │ │└rewrite ?EtaInterp.InterpExprEta 4.7% 4.7% 1 0.316s │ │ ├─Reify.transitivity_tt ----------- 0.1% 2.6% 2 0.116s │ │ ├─rewrite H ----------------------- 2.6% 2.6% 1 0.172s │ │ └─tac ----------------------------- 1.5% 2.3% 1 0.156s │ └─ReflectiveTactics.solve_post_reifie 0.6% 31.7% 1 2.132s │ ├─UnifyAbstractReflexivity.unify_tr 21.7% 25.8% 7 0.424s │ │└unify (constr) (constr) --------- 3.1% 3.1% 5 0.084s │ └─ReflectiveTactics.unify_abstract_ 3.4% 5.0% 1 0.336s └─Glue.refine_to_reflective_glue' ----- 0.0% 6.5% 1 0.436s └Glue.zrange_to_reflective ----------- 0.0% 4.2% 1 0.280s └Glue.zrange_to_reflective_goal ------ 2.4% 3.3% 1 0.220s src/Specific/X25519/C64/freeze (real: 34.35, user: 31.50, sys: 0.24, mem: 828104 ko) COQC src/Specific/NISTP256/AMD64/feadd.v Finished transaction in 8.784 secs (8.176u,0.011s) (successful) total time: 8.140s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 52.4% 1 4.268s ─synthesize_montgomery ----------------- 0.0% 47.6% 1 3.872s ─ReflectiveTactics.do_reflective_pipelin 0.0% 43.8% 1 3.568s ─ReflectiveTactics.solve_side_conditions 0.0% 43.2% 1 3.520s ─IntegrationTestTemporaryMiscCommon.fact 1.4% 23.6% 1 1.924s ─IntegrationTestTemporaryMiscCommon.do_r 0.0% 22.1% 1 1.796s ─ReflectiveTactics.do_reify ------------ 0.1% 21.7% 1 1.768s ─ReflectiveTactics.solve_post_reified_si 0.6% 21.5% 1 1.752s ─Reify.Reify_rhs_gen ------------------- 1.0% 20.9% 1 1.704s ─op_sig_side_conditions_t -------------- 0.0% 20.0% 1 1.624s ─DestructHyps.do_all_matches_then ------ 0.0% 20.0% 8 0.244s ─DestructHyps.do_one_match_then -------- 0.7% 19.9% 44 0.052s ─do_tac -------------------------------- 0.0% 19.2% 36 0.052s ─destruct H ---------------------------- 19.2% 19.2% 36 0.052s ─rewrite <- (lem : lemT) by by_tac ltac: 0.2% 17.3% 1 1.408s ─IntegrationTestTemporaryMiscCommon.do_r 0.0% 17.3% 1 1.408s ─by_tac -------------------------------- 0.0% 17.1% 4 0.504s ─rewrite <- (ZRange.is_bounded_by_None_r 16.7% 16.7% 8 0.344s ─UnifyAbstractReflexivity.unify_transfor 13.3% 16.1% 7 0.360s ─Reify.do_reify_abs_goal --------------- 9.9% 10.1% 2 0.820s ─Reify.do_reifyf_goal ------------------ 9.1% 9.3% 93 0.748s ─Glue.refine_to_reflective_glue' ------- 0.0% 8.6% 1 0.700s ─Glue.zrange_to_reflective ------------- 0.0% 5.3% 1 0.432s ─IntegrationTestTemporaryMiscCommon.do_s 0.0% 4.8% 1 0.388s ─ MapProjections.proj2 2.4% 2.4% 2 0.120s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 52.4% 1 4.268s ├─ReflectiveTactics.do_reflective_pipel 0.0% 43.8% 1 3.568s │└ReflectiveTactics.solve_side_conditio 0.0% 43.2% 1 3.520s │ ├─ReflectiveTactics.do_reify -------- 0.1% 21.7% 1 1.768s │ │└Reify.Reify_rhs_gen --------------- 1.0% 20.9% 1 1.704s │ │ ├─Reify.do_reify_abs_goal --------- 9.9% 10.1% 2 0.820s │ │ │└Reify.do_reifyf_goal ------------ 9.1% 9.3% 93 0.748s │ │ │└eexact -------------------------- 2.3% 2.3% 93 0.024s │ │ ├─prove_interp_compile_correct ---- 0.0% 2.5% 1 0.204s │ │ └─rewrite H ----------------------- 2.4% 2.4% 1 0.196s │ └─ReflectiveTactics.solve_post_reifie 0.6% 21.5% 1 1.752s │ ├─UnifyAbstractReflexivity.unify_tr 13.3% 16.1% 7 0.360s │ │└unify (constr) (constr) --------- 2.2% 2.2% 5 0.064s │ └─ReflectiveTactics.unify_abstract_ 3.3% 4.5% 1 0.368s └─Glue.refine_to_reflective_glue' ----- 0.0% 8.6% 1 0.700s └Glue.zrange_to_reflective ----------- 0.0% 5.3% 1 0.432s └Glue.zrange_to_reflective_goal ------ 2.6% 4.0% 1 0.324s ─synthesize_montgomery ----------------- 0.0% 47.6% 1 3.872s ├─IntegrationTestTemporaryMiscCommon.fa 1.4% 23.6% 1 1.924s │└op_sig_side_conditions_t ------------ 0.0% 20.0% 1 1.624s │ ├─DestructHyps.do_all_matches_then -- 0.0% 11.4% 4 0.244s │ │└DestructHyps.do_one_match_then ---- 0.3% 11.4% 24 0.052s │ │└do_tac ---------------------------- 0.0% 11.1% 20 0.052s │ │└destruct H ------------------------ 11.1% 11.1% 20 0.052s │ └─rewrite <- (ZRange.is_bounded_by_No 8.4% 8.4% 4 0.328s └─IntegrationTestTemporaryMiscCommon.do 0.0% 22.1% 1 1.796s ├─IntegrationTestTemporaryMiscCommon. 0.0% 17.3% 1 1.408s │└rewrite <- (lem : lemT) by by_tac l 0.2% 17.3% 1 1.408s │└by_tac ---------------------------- 0.0% 17.1% 4 0.504s │ ├─DestructHyps.do_all_matches_then 0.0% 8.6% 4 0.184s │ │└DestructHyps.do_one_match_then -- 0.3% 8.5% 20 0.052s │ │└do_tac -------------------------- 0.0% 8.2% 16 0.052s │ │└destruct H ---------------------- 8.2% 8.2% 16 0.052s │ └─rewrite <- (ZRange.is_bounded_by_ 8.3% 8.3% 4 0.344s └─IntegrationTestTemporaryMiscCommon. 0.0% 4.8% 1 0.388s └ MapProjections.proj2 2.4% 2.4% 2 0.120s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 52.4% 1 4.268s ├─ReflectiveTactics.do_reflective_pipel 0.0% 43.8% 1 3.568s │└ReflectiveTactics.solve_side_conditio 0.0% 43.2% 1 3.520s │ ├─ReflectiveTactics.do_reify -------- 0.1% 21.7% 1 1.768s │ │└Reify.Reify_rhs_gen --------------- 1.0% 20.9% 1 1.704s │ │ ├─Reify.do_reify_abs_goal --------- 9.9% 10.1% 2 0.820s │ │ │└Reify.do_reifyf_goal ------------ 9.1% 9.3% 93 0.748s │ │ │└eexact -------------------------- 2.3% 2.3% 93 0.024s │ │ ├─prove_interp_compile_correct ---- 0.0% 2.5% 1 0.204s │ │ └─rewrite H ----------------------- 2.4% 2.4% 1 0.196s │ └─ReflectiveTactics.solve_post_reifie 0.6% 21.5% 1 1.752s │ ├─UnifyAbstractReflexivity.unify_tr 13.3% 16.1% 7 0.360s │ │└unify (constr) (constr) --------- 2.2% 2.2% 5 0.064s │ └─ReflectiveTactics.unify_abstract_ 3.3% 4.5% 1 0.368s └─Glue.refine_to_reflective_glue' ----- 0.0% 8.6% 1 0.700s └Glue.zrange_to_reflective ----------- 0.0% 5.3% 1 0.432s └Glue.zrange_to_reflective_goal ------ 2.6% 4.0% 1 0.324s ─synthesize_montgomery ----------------- 0.0% 47.6% 1 3.872s ├─IntegrationTestTemporaryMiscCommon.fa 1.4% 23.6% 1 1.924s │└op_sig_side_conditions_t ------------ 0.0% 20.0% 1 1.624s │ ├─DestructHyps.do_all_matches_then -- 0.0% 11.4% 4 0.244s │ │└DestructHyps.do_one_match_then ---- 0.3% 11.4% 24 0.052s │ │└do_tac ---------------------------- 0.0% 11.1% 20 0.052s │ │└destruct H ------------------------ 11.1% 11.1% 20 0.052s │ └─rewrite <- (ZRange.is_bounded_by_No 8.4% 8.4% 4 0.328s └─IntegrationTestTemporaryMiscCommon.do 0.0% 22.1% 1 1.796s ├─IntegrationTestTemporaryMiscCommon. 0.0% 17.3% 1 1.408s │└rewrite <- (lem : lemT) by by_tac l 0.2% 17.3% 1 1.408s │└by_tac ---------------------------- 0.0% 17.1% 4 0.504s │ ├─DestructHyps.do_all_matches_then 0.0% 8.6% 4 0.184s │ │└DestructHyps.do_one_match_then -- 0.3% 8.5% 20 0.052s │ │└do_tac -------------------------- 0.0% 8.2% 16 0.052s │ │└destruct H ---------------------- 8.2% 8.2% 16 0.052s │ └─rewrite <- (ZRange.is_bounded_by_ 8.3% 8.3% 4 0.344s └─IntegrationTestTemporaryMiscCommon. 0.0% 4.8% 1 0.388s └ src/Specific/NISTP256/AMD64/feaddDisplay.log COQC src/Specific/NISTP256/AMD64/fenzDisplay > src/Specific/NISTP256/AMD64/fenzDisplay.log COQC src/Specific/solinas32_2e255m765_12limbs/femul.v Finished transaction in 50.426 secs (46.528u,0.072s) (successful) total time: 46.544s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ -0.0% 94.9% 1 44.164s ─ReflectiveTactics.do_reflective_pipelin 0.0% 87.1% 1 40.552s ─ReflectiveTactics.solve_side_conditions 0.0% 86.7% 1 40.372s ─ReflectiveTactics.do_reify ------------ 0.0% 59.6% 1 27.740s ─Reify.Reify_rhs_gen ------------------- 1.6% 58.9% 1 27.432s ─Reify.do_reify_abs_goal --------------- 43.3% 43.6% 2 20.312s ─Reify.do_reifyf_goal ------------------ 42.5% 42.8% 108 10.328s ─ReflectiveTactics.solve_post_reified_si 0.1% 27.1% 1 12.632s ─UnifyAbstractReflexivity.unify_transfor 18.6% 23.5% 7 3.552s ─eexact -------------------------------- 13.7% 13.7% 110 0.136s ─Glue.refine_to_reflective_glue' ------- 0.0% 7.8% 1 3.612s ─Glue.zrange_to_reflective ------------- 0.0% 7.2% 1 3.332s ─Glue.zrange_to_reflective_goal -------- 1.7% 5.5% 1 2.544s ─synthesize ---------------------------- 0.0% 5.1% 1 2.380s ─unify (constr) (constr) --------------- 5.1% 5.1% 6 1.068s ─IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.0% 1 2.320s ─change G' ----------------------------- 4.8% 4.8% 1 2.252s ─rewrite H ----------------------------- 3.8% 3.8% 1 1.748s ─pose proof (pf : Interpretation.Bo 3.6% 3.6% 1 1.664s ─prove_interp_compile_correct ---------- 0.0% 3.5% 1 1.616s ─rewrite ?EtaInterp.InterpExprEta ------ 3.2% 3.2% 1 1.468s ─ReflectiveTactics.unify_abstract_cbv_in 1.6% 2.4% 1 1.124s ─reflexivity --------------------------- 2.1% 2.1% 7 0.396s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ -0.0% 94.9% 1 44.164s ├─ReflectiveTactics.do_reflective_pipel 0.0% 87.1% 1 40.552s │└ReflectiveTactics.solve_side_conditio 0.0% 86.7% 1 40.372s │ ├─ReflectiveTactics.do_reify -------- 0.0% 59.6% 1 27.740s │ │└Reify.Reify_rhs_gen --------------- 1.6% 58.9% 1 27.432s │ │ ├─Reify.do_reify_abs_goal --------- 43.3% 43.6% 2 20.312s │ │ │└Reify.do_reifyf_goal ------------ 42.5% 42.8% 108 10.328s │ │ │└eexact -------------------------- 13.2% 13.2% 108 0.072s │ │ ├─rewrite H ----------------------- 3.8% 3.8% 1 1.748s │ │ └─prove_interp_compile_correct ---- 0.0% 3.5% 1 1.616s │ │ └rewrite ?EtaInterp.InterpExprEta 3.2% 3.2% 1 1.468s │ └─ReflectiveTactics.solve_post_reifie 0.1% 27.1% 1 12.632s │ ├─UnifyAbstractReflexivity.unify_tr 18.6% 23.5% 7 3.552s │ │└unify (constr) (constr) --------- 4.3% 4.3% 5 1.068s │ └─ReflectiveTactics.unify_abstract_ 1.6% 2.4% 1 1.124s └─Glue.refine_to_reflective_glue' ----- 0.0% 7.8% 1 3.612s └Glue.zrange_to_reflective ----------- 0.0% 7.2% 1 3.332s └Glue.zrange_to_reflective_goal ------ 1.7% 5.5% 1 2.544s └pose proof (pf : Interpretation. 3.6% 3.6% 1 1.664s ─synthesize ---------------------------- 0.0% 5.1% 1 2.380s └IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.0% 1 2.320s └change G' ----------------------------- 4.8% 4.8% 1 2.252s Finished transaction in 80.129 secs (74.068u,0.024s) (successful) Closed under the global context total time: 46.544s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ -0.0% 94.9% 1 44.164s ─ReflectiveTactics.do_reflective_pipelin 0.0% 87.1% 1 40.552s ─ReflectiveTactics.solve_side_conditions 0.0% 86.7% 1 40.372s ─ReflectiveTactics.do_reify ------------ 0.0% 59.6% 1 27.740s ─Reify.Reify_rhs_gen ------------------- 1.6% 58.9% 1 27.432s ─Reify.do_reify_abs_goal --------------- 43.3% 43.6% 2 20.312s ─Reify.do_reifyf_goal ------------------ 42.5% 42.8% 108 10.328s ─ReflectiveTactics.solve_post_reified_si 0.1% 27.1% 1 12.632s ─UnifyAbstractReflexivity.unify_transfor 18.6% 23.5% 7 3.552s ─eexact -------------------------------- 13.7% 13.7% 110 0.136s ─Glue.refine_to_reflective_glue' ------- 0.0% 7.8% 1 3.612s ─Glue.zrange_to_reflective ------------- 0.0% 7.2% 1 3.332s ─Glue.zrange_to_reflective_goal -------- 1.7% 5.5% 1 2.544s ─synthesize ---------------------------- 0.0% 5.1% 1 2.380s ─unify (constr) (constr) --------------- 5.1% 5.1% 6 1.068s ─IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.0% 1 2.320s ─change G' ----------------------------- 4.8% 4.8% 1 2.252s ─rewrite H ----------------------------- 3.8% 3.8% 1 1.748s ─pose proof (pf : Interpretation.Bo 3.6% 3.6% 1 1.664s ─prove_interp_compile_correct ---------- 0.0% 3.5% 1 1.616s ─rewrite ?EtaInterp.InterpExprEta ------ 3.2% 3.2% 1 1.468s ─ReflectiveTactics.unify_abstract_cbv_in 1.6% 2.4% 1 1.124s ─reflexivity --------------------------- 2.1% 2.1% 7 0.396s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ -0.0% 94.9% 1 44.164s ├─ReflectiveTactics.do_reflective_pipel 0.0% 87.1% 1 40.552s │└ReflectiveTactics.solve_side_conditio 0.0% 86.7% 1 40.372s │ ├─ReflectiveTactics.do_reify -------- 0.0% 59.6% 1 27.740s │ │└Reify.Reify_rhs_gen --------------- 1.6% 58.9% 1 27.432s │ │ ├─Reify.do_reify_abs_goal --------- 43.3% 43.6% 2 20.312s │ │ │└Reify.do_reifyf_goal ------------ 42.5% 42.8% 108 10.328s │ │ │└eexact -------------------------- 13.2% 13.2% 108 0.072s │ │ ├─rewrite H ----------------------- 3.8% 3.8% 1 1.748s │ │ └─prove_interp_compile_correct ---- 0.0% 3.5% 1 1.616s │ │ └rewrite ?EtaInterp.InterpExprEta 3.2% 3.2% 1 1.468s │ └─ReflectiveTactics.solve_post_reifie 0.1% 27.1% 1 12.632s │ ├─UnifyAbstractReflexivity.unify_tr 18.6% 23.5% 7 3.552s │ │└unify (constr) (constr) --------- 4.3% 4.3% 5 1.068s │ └─ReflectiveTactics.unify_abstract_ 1.6% 2.4% 1 1.124s └─Glue.refine_to_reflective_glue' ----- 0.0% 7.8% 1 3.612s └Glue.zrange_to_reflective ----------- 0.0% 7.2% 1 3.332s └Glue.zrange_to_reflective_goal ------ 1.7% 5.5% 1 2.544s └pose proof (pf : Interpretation. 3.6% 3.6% 1 1.664s ─synthesize ---------------------------- 0.0% 5.1% 1 2.380s └IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.0% 1 2.320s └change G' ----------------------------- 4.8% 4.8% 1 2.252s src/Specific/solinas32_2e255m765_12limbs/femul (real: 155.79, user: 143.70, sys: 0.32, mem: 1454696 ko) COQC src/Specific/NISTP256/AMD64/feoppDisplay > src/Specific/NISTP256/AMD64/feoppDisplay.log COQC src/Specific/NISTP256/AMD64/fesubDisplay > src/Specific/NISTP256/AMD64/fesubDisplay.log COQC src/Specific/X25519/C64/fesquareDisplay > src/Specific/X25519/C64/fesquareDisplay.log COQC src/Specific/X25519/C64/fesubDisplay > src/Specific/X25519/C64/fesubDisplay.log COQC src/Specific/X25519/C64/freezeDisplay > src/Specific/X25519/C64/freezeDisplay.log COQC src/Specific/solinas32_2e255m765_13limbs/femul.v Finished transaction in 61.854 secs (57.328u,0.079s) (successful) total time: 57.348s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.6% 1 54.224s ─ReflectiveTactics.do_reflective_pipelin 0.0% 86.2% 1 49.452s ─ReflectiveTactics.solve_side_conditions 0.0% 85.9% 1 49.264s ─ReflectiveTactics.do_reify ------------ -0.0% 57.6% 1 33.004s ─Reify.Reify_rhs_gen ------------------- 1.3% 56.9% 1 32.608s ─Reify.do_reify_abs_goal --------------- 43.1% 43.3% 2 24.840s ─Reify.do_reifyf_goal ------------------ 42.3% 42.6% 117 12.704s ─ReflectiveTactics.solve_post_reified_si 0.1% 28.4% 1 16.260s ─UnifyAbstractReflexivity.unify_transfor 19.6% 25.0% 7 4.824s ─eexact -------------------------------- 13.9% 13.9% 119 0.144s ─Glue.refine_to_reflective_glue' ------- 0.0% 8.3% 1 4.772s ─Glue.zrange_to_reflective ------------- 0.0% 7.8% 1 4.484s ─Glue.zrange_to_reflective_goal -------- 1.7% 6.0% 1 3.464s ─synthesize ---------------------------- 0.0% 5.4% 1 3.124s ─unify (constr) (constr) --------------- 5.4% 5.4% 6 1.540s ─IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.3% 1 3.040s ─change G' ----------------------------- 5.2% 5.2% 1 2.964s ─pose proof (pf : Interpretation.Bo 4.2% 4.2% 1 2.416s ─prove_interp_compile_correct ---------- 0.0% 3.3% 1 1.904s ─rewrite H ----------------------------- 3.3% 3.3% 1 1.896s ─rewrite ?EtaInterp.InterpExprEta ------ 3.0% 3.0% 1 1.732s ─ReflectiveTactics.unify_abstract_cbv_in 1.4% 2.1% 1 1.212s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.6% 1 54.224s ├─ReflectiveTactics.do_reflective_pipel 0.0% 86.2% 1 49.452s │└ReflectiveTactics.solve_side_conditio 0.0% 85.9% 1 49.264s │ ├─ReflectiveTactics.do_reify -------- -0.0% 57.6% 1 33.004s │ │└Reify.Reify_rhs_gen --------------- 1.3% 56.9% 1 32.608s │ │ ├─Reify.do_reify_abs_goal --------- 43.1% 43.3% 2 24.840s │ │ │└Reify.do_reifyf_goal ------------ 42.3% 42.6% 117 12.704s │ │ │└eexact -------------------------- 13.4% 13.4% 117 0.084s │ │ ├─prove_interp_compile_correct ---- 0.0% 3.3% 1 1.904s │ │ │└rewrite ?EtaInterp.InterpExprEta 3.0% 3.0% 1 1.732s │ │ └─rewrite H ----------------------- 3.3% 3.3% 1 1.896s │ └─ReflectiveTactics.solve_post_reifie 0.1% 28.4% 1 16.260s │ ├─UnifyAbstractReflexivity.unify_tr 19.6% 25.0% 7 4.824s │ │└unify (constr) (constr) --------- 4.8% 4.8% 5 1.540s │ └─ReflectiveTactics.unify_abstract_ 1.4% 2.1% 1 1.212s └─Glue.refine_to_reflective_glue' ----- 0.0% 8.3% 1 4.772s └Glue.zrange_to_reflective ----------- 0.0% 7.8% 1 4.484s └Glue.zrange_to_reflective_goal ------ 1.7% 6.0% 1 3.464s └pose proof (pf : Interpretation. 4.2% 4.2% 1 2.416s ─synthesize ---------------------------- 0.0% 5.4% 1 3.124s └IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.3% 1 3.040s └change G' ----------------------------- 5.2% 5.2% 1 2.964s Finished transaction in 94.432 secs (86.96u,0.02s) (successful) Closed under the global context total time: 57.348s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.6% 1 54.224s ─ReflectiveTactics.do_reflective_pipelin 0.0% 86.2% 1 49.452s ─ReflectiveTactics.solve_side_conditions 0.0% 85.9% 1 49.264s ─ReflectiveTactics.do_reify ------------ -0.0% 57.6% 1 33.004s ─Reify.Reify_rhs_gen ------------------- 1.3% 56.9% 1 32.608s ─Reify.do_reify_abs_goal --------------- 43.1% 43.3% 2 24.840s ─Reify.do_reifyf_goal ------------------ 42.3% 42.6% 117 12.704s ─ReflectiveTactics.solve_post_reified_si 0.1% 28.4% 1 16.260s ─UnifyAbstractReflexivity.unify_transfor 19.6% 25.0% 7 4.824s ─eexact -------------------------------- 13.9% 13.9% 119 0.144s ─Glue.refine_to_reflective_glue' ------- 0.0% 8.3% 1 4.772s ─Glue.zrange_to_reflective ------------- 0.0% 7.8% 1 4.484s ─Glue.zrange_to_reflective_goal -------- 1.7% 6.0% 1 3.464s ─synthesize ---------------------------- 0.0% 5.4% 1 3.124s ─unify (constr) (constr) --------------- 5.4% 5.4% 6 1.540s ─IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.3% 1 3.040s ─change G' ----------------------------- 5.2% 5.2% 1 2.964s ─pose proof (pf : Interpretation.Bo 4.2% 4.2% 1 2.416s ─prove_interp_compile_correct ---------- 0.0% 3.3% 1 1.904s ─rewrite H ----------------------------- 3.3% 3.3% 1 1.896s ─rewrite ?EtaInterp.InterpExprEta ------ 3.0% 3.0% 1 1.732s ─ReflectiveTactics.unify_abstract_cbv_in 1.4% 2.1% 1 1.212s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 94.6% 1 54.224s ├─ReflectiveTactics.do_reflective_pipel 0.0% 86.2% 1 49.452s │└ReflectiveTactics.solve_side_conditio 0.0% 85.9% 1 49.264s │ ├─ReflectiveTactics.do_reify -------- -0.0% 57.6% 1 33.004s │ │└Reify.Reify_rhs_gen --------------- 1.3% 56.9% 1 32.608s │ │ ├─Reify.do_reify_abs_goal --------- 43.1% 43.3% 2 24.840s │ │ │└Reify.do_reifyf_goal ------------ 42.3% 42.6% 117 12.704s │ │ │└eexact -------------------------- 13.4% 13.4% 117 0.084s │ │ ├─prove_interp_compile_correct ---- 0.0% 3.3% 1 1.904s │ │ │└rewrite ?EtaInterp.InterpExprEta 3.0% 3.0% 1 1.732s │ │ └─rewrite H ----------------------- 3.3% 3.3% 1 1.896s │ └─ReflectiveTactics.solve_post_reifie 0.1% 28.4% 1 16.260s │ ├─UnifyAbstractReflexivity.unify_tr 19.6% 25.0% 7 4.824s │ │└unify (constr) (constr) --------- 4.8% 4.8% 5 1.540s │ └─ReflectiveTactics.unify_abstract_ 1.4% 2.1% 1 1.212s └─Glue.refine_to_reflective_glue' ----- 0.0% 8.3% 1 4.772s └Glue.zrange_to_reflective ----------- 0.0% 7.8% 1 4.484s └Glue.zrange_to_reflective_goal ------ 1.7% 6.0% 1 3.464s └pose proof (pf : Interpretation. 4.2% 4.2% 1 2.416s ─synthesize ---------------------------- 0.0% 5.4% 1 3.124s └IntegrationTestTemporaryMiscCommon.do_r 0.0% 5.3% 1 3.040s └change G' ----------------------------- 5.2% 5.2% 1 2.964s src/Specific/solinas32_2e255m765_13limbs/femul (real: 181.77, user: 168.52, sys: 0.40, mem: 1589516 ko) COQC src/Specific/NISTP256/AMD64/femul.v Finished transaction in 119.257 secs (109.936u,0.256s) (successful) total time: 110.140s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.1% 1 106.964s ─ReflectiveTactics.do_reflective_pipelin -0.0% 96.4% 1 106.196s ─ReflectiveTactics.solve_side_conditions 0.0% 96.2% 1 105.992s ─ReflectiveTactics.do_reify ------------ -0.0% 83.7% 1 92.208s ─Reify.Reify_rhs_gen ------------------- 0.7% 83.5% 1 91.960s ─Reify.do_reify_abs_goal --------------- 77.7% 77.8% 2 85.708s ─Reify.do_reifyf_goal ------------------ 77.4% 77.5% 901 85.364s ─eexact -------------------------------- 17.9% 17.9% 903 0.136s ─ReflectiveTactics.solve_post_reified_si 0.3% 12.5% 1 13.784s ─UnifyAbstractReflexivity.unify_transfor 9.8% 11.2% 7 3.356s ─synthesize_montgomery ----------------- 0.0% 2.9% 1 3.176s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.1% 1 106.964s └ReflectiveTactics.do_reflective_pipelin -0.0% 96.4% 1 106.196s └ReflectiveTactics.solve_side_conditions 0.0% 96.2% 1 105.992s ├─ReflectiveTactics.do_reify ---------- -0.0% 83.7% 1 92.208s │└Reify.Reify_rhs_gen ----------------- 0.7% 83.5% 1 91.960s │└Reify.do_reify_abs_goal ------------- 77.7% 77.8% 2 85.708s │└Reify.do_reifyf_goal ---------------- 77.4% 77.5% 901 85.364s │└eexact ------------------------------ 17.7% 17.7% 901 0.136s └─ReflectiveTactics.solve_post_reified_ 0.3% 12.5% 1 13.784s └UnifyAbstractReflexivity.unify_transf 9.8% 11.2% 7 3.356s ─synthesize_montgomery ----------------- 0.0% 2.9% 1 3.176s Finished transaction in 61.452 secs (58.503u,0.055s) (successful) Closed under the global context total time: 110.140s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.1% 1 106.964s ─ReflectiveTactics.do_reflective_pipelin -0.0% 96.4% 1 106.196s ─ReflectiveTactics.solve_side_conditions 0.0% 96.2% 1 105.992s ─ReflectiveTactics.do_reify ------------ -0.0% 83.7% 1 92.208s ─Reify.Reify_rhs_gen ------------------- 0.7% 83.5% 1 91.960s ─Reify.do_reify_abs_goal --------------- 77.7% 77.8% 2 85.708s ─Reify.do_reifyf_goal ------------------ 77.4% 77.5% 901 85.364s ─eexact -------------------------------- 17.9% 17.9% 903 0.136s ─ReflectiveTactics.solve_post_reified_si 0.3% 12.5% 1 13.784s ─UnifyAbstractReflexivity.unify_transfor 9.8% 11.2% 7 3.356s ─synthesize_montgomery ----------------- 0.0% 2.9% 1 3.176s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─Pipeline.refine_reflectively_gen ------ 0.0% 97.1% 1 106.964s └ReflectiveTactics.do_reflective_pipelin -0.0% 96.4% 1 106.196s └ReflectiveTactics.solve_side_conditions 0.0% 96.2% 1 105.992s ├─ReflectiveTactics.do_reify ---------- -0.0% 83.7% 1 92.208s │└Reify.Reify_rhs_gen ----------------- 0.7% 83.5% 1 91.960s │└Reify.do_reify_abs_goal ------------- 77.7% 77.8% 2 85.708s │└Reify.do_reifyf_goal ---------------- 77.4% 77.5% 901 85.364s │└eexact ------------------------------ 17.7% 17.7% 901 0.136s └─ReflectiveTactics.solve_post_reified_ 0.3% 12.5% 1 13.784s └UnifyAbstractReflexivity.unify_transf 9.8% 11.2% 7 3.356s ─synthesize_montgomery ----------------- 0.0% 2.9% 1 3.176s src/Specific/NISTP256/AMD64/femul (real: 202.96, user: 189.62, sys: 0.64, mem: 3302508 ko) COQC src/Specific/NISTP256/AMD64/femulDisplay > src/Specific/NISTP256/AMD64/femulDisplay.log COQC src/Specific/X25519/C64/ladderstep.v total time: 52.080s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_xzladderstep --------------- 0.0% 100.0% 1 52.080s ─Pipeline.refine_reflectively_gen ------ 0.0% 98.5% 1 51.320s ─ReflectiveTactics.do_reflective_pipelin 0.0% 93.8% 1 48.872s ─ReflectiveTactics.solve_side_conditions 0.0% 93.7% 1 48.776s ─ReflectiveTactics.solve_post_reified_si 0.2% 56.5% 1 29.412s ─UnifyAbstractReflexivity.unify_transfor 44.7% 49.1% 7 6.968s ─ReflectiveTactics.do_reify ------------ 0.0% 37.2% 1 19.364s ─Reify.Reify_rhs_gen ------------------- 2.1% 23.4% 1 12.200s ─Reify.do_reifyf_goal ------------------ 11.2% 11.3% 138 1.884s ─Compilers.Reify.reify_context_variables 0.1% 9.2% 1 4.808s ─rewrite H ----------------------------- 7.3% 7.3% 1 3.816s ─ReflectiveTactics.unify_abstract_cbv_in 4.7% 6.4% 1 3.336s ─Glue.refine_to_reflective_glue' ------- 0.0% 4.7% 1 2.448s ─Glue.zrange_to_reflective ------------- 0.0% 4.0% 1 2.068s ─Reify.transitivity_tt ----------------- 0.1% 3.7% 2 0.984s ─transitivity -------------------------- 3.5% 3.5% 10 0.880s ─reflexivity --------------------------- 3.4% 3.4% 11 0.772s ─Glue.zrange_to_reflective_goal -------- 2.4% 3.3% 1 1.728s ─eexact -------------------------------- 3.2% 3.2% 140 0.032s ─unify (constr) (constr) --------------- 3.1% 3.1% 6 0.852s ─clear (var_list) ---------------------- 3.1% 3.1% 98 0.584s ─UnfoldArg.unfold_second_arg ----------- 0.4% 3.0% 2 1.576s ─tac ----------------------------------- 2.1% 3.0% 2 1.564s ─ClearAll.clear_all -------------------- 0.2% 2.8% 7 0.584s ─ChangeInAll.change_with_compute_in_all 0.0% 2.6% 221 0.012s ─change c with c' in * ----------------- 2.5% 2.5% 221 0.012s ─Reify.do_reify_abs_goal --------------- 2.4% 2.5% 2 1.276s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_xzladderstep --------------- 0.0% 100.0% 1 52.080s └Pipeline.refine_reflectively_gen ------ 0.0% 98.5% 1 51.320s ├─ReflectiveTactics.do_reflective_pipel 0.0% 93.8% 1 48.872s │└ReflectiveTactics.solve_side_conditio 0.0% 93.7% 1 48.776s │ ├─ReflectiveTactics.solve_post_reifie 0.2% 56.5% 1 29.412s │ │ ├─UnifyAbstractReflexivity.unify_tr 44.7% 49.1% 7 6.968s │ │ │└ClearAll.clear_all -------------- 0.2% 2.8% 7 0.584s │ │ │└clear (var_list) ---------------- 2.7% 2.7% 65 0.584s │ │ └─ReflectiveTactics.unify_abstract_ 4.7% 6.4% 1 3.336s │ └─ReflectiveTactics.do_reify -------- 0.0% 37.2% 1 19.364s │ ├─Reify.Reify_rhs_gen ------------- 2.1% 23.4% 1 12.200s │ │ ├─rewrite H --------------------- 7.3% 7.3% 1 3.816s │ │ ├─Reify.transitivity_tt --------- 0.1% 3.7% 2 0.984s │ │ │└transitivity ------------------ 3.4% 3.4% 4 0.880s │ │ ├─tac --------------------------- 2.1% 3.0% 1 1.564s │ │ └─Reify.do_reify_abs_goal ------- 2.4% 2.5% 2 1.276s │ │ └Reify.do_reifyf_goal ---------- 2.2% 2.2% 25 1.148s │ ├─Compilers.Reify.reify_context_var 0.1% 9.2% 1 4.808s │ │└Reify.do_reifyf_goal ------------ 9.0% 9.1% 113 1.884s │ │└eexact -------------------------- 2.4% 2.4% 113 0.032s │ └─UnfoldArg.unfold_second_arg ----- 0.4% 3.0% 2 1.576s │ └ChangeInAll.change_with_compute_i 0.0% 2.6% 221 0.012s │ └change c with c' in * ----------- 2.5% 2.5% 221 0.012s └─Glue.refine_to_reflective_glue' ----- 0.0% 4.7% 1 2.448s └Glue.zrange_to_reflective ----------- 0.0% 4.0% 1 2.068s └Glue.zrange_to_reflective_goal ------ 2.4% 3.3% 1 1.728s Finished transaction in 171.122 secs (161.392u,0.039s) (successful) Closed under the global context total time: 52.080s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_xzladderstep --------------- 0.0% 100.0% 1 52.080s ─Pipeline.refine_reflectively_gen ------ 0.0% 98.5% 1 51.320s ─ReflectiveTactics.do_reflective_pipelin 0.0% 93.8% 1 48.872s ─ReflectiveTactics.solve_side_conditions 0.0% 93.7% 1 48.776s ─ReflectiveTactics.solve_post_reified_si 0.2% 56.5% 1 29.412s ─UnifyAbstractReflexivity.unify_transfor 44.7% 49.1% 7 6.968s ─ReflectiveTactics.do_reify ------------ 0.0% 37.2% 1 19.364s ─Reify.Reify_rhs_gen ------------------- 2.1% 23.4% 1 12.200s ─Reify.do_reifyf_goal ------------------ 11.2% 11.3% 138 1.884s ─Compilers.Reify.reify_context_variables 0.1% 9.2% 1 4.808s ─rewrite H ----------------------------- 7.3% 7.3% 1 3.816s ─ReflectiveTactics.unify_abstract_cbv_in 4.7% 6.4% 1 3.336s ─Glue.refine_to_reflective_glue' ------- 0.0% 4.7% 1 2.448s ─Glue.zrange_to_reflective ------------- 0.0% 4.0% 1 2.068s ─Reify.transitivity_tt ----------------- 0.1% 3.7% 2 0.984s ─transitivity -------------------------- 3.5% 3.5% 10 0.880s ─reflexivity --------------------------- 3.4% 3.4% 11 0.772s ─Glue.zrange_to_reflective_goal -------- 2.4% 3.3% 1 1.728s ─eexact -------------------------------- 3.2% 3.2% 140 0.032s ─unify (constr) (constr) --------------- 3.1% 3.1% 6 0.852s ─clear (var_list) ---------------------- 3.1% 3.1% 98 0.584s ─UnfoldArg.unfold_second_arg ----------- 0.4% 3.0% 2 1.576s ─tac ----------------------------------- 2.1% 3.0% 2 1.564s ─ClearAll.clear_all -------------------- 0.2% 2.8% 7 0.584s ─ChangeInAll.change_with_compute_in_all 0.0% 2.6% 221 0.012s ─change c with c' in * ----------------- 2.5% 2.5% 221 0.012s ─Reify.do_reify_abs_goal --------------- 2.4% 2.5% 2 1.276s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─synthesize_xzladderstep --------------- 0.0% 100.0% 1 52.080s └Pipeline.refine_reflectively_gen ------ 0.0% 98.5% 1 51.320s ├─ReflectiveTactics.do_reflective_pipel 0.0% 93.8% 1 48.872s │└ReflectiveTactics.solve_side_conditio 0.0% 93.7% 1 48.776s │ ├─ReflectiveTactics.solve_post_reifie 0.2% 56.5% 1 29.412s │ │ ├─UnifyAbstractReflexivity.unify_tr 44.7% 49.1% 7 6.968s │ │ │└ClearAll.clear_all -------------- 0.2% 2.8% 7 0.584s │ │ │└clear (var_list) ---------------- 2.7% 2.7% 65 0.584s │ │ └─ReflectiveTactics.unify_abstract_ 4.7% 6.4% 1 3.336s │ └─ReflectiveTactics.do_reify -------- 0.0% 37.2% 1 19.364s │ ├─Reify.Reify_rhs_gen ------------- 2.1% 23.4% 1 12.200s │ │ ├─rewrite H --------------------- 7.3% 7.3% 1 3.816s │ │ ├─Reify.transitivity_tt --------- 0.1% 3.7% 2 0.984s │ │ │└transitivity ------------------ 3.4% 3.4% 4 0.880s │ │ ├─tac --------------------------- 2.1% 3.0% 1 1.564s │ │ └─Reify.do_reify_abs_goal ------- 2.4% 2.5% 2 1.276s │ │ └Reify.do_reifyf_goal ---------- 2.2% 2.2% 25 1.148s │ ├─Compilers.Reify.reify_context_var 0.1% 9.2% 1 4.808s │ │└Reify.do_reifyf_goal ------------ 9.0% 9.1% 113 1.884s │ │└eexact -------------------------- 2.4% 2.4% 113 0.032s │ └─UnfoldArg.unfold_second_arg ----- 0.4% 3.0% 2 1.576s │ └ChangeInAll.change_with_compute_i 0.0% 2.6% 221 0.012s │ └change c with c' in * ----------- 2.5% 2.5% 221 0.012s └─Glue.refine_to_reflective_glue' ----- 0.0% 4.7% 1 2.448s └Glue.zrange_to_reflective ----------- 0.0% 4.0% 1 2.068s └Glue.zrange_to_reflective_goal ------ 2.4% 3.3% 1 1.728s src/Specific/X25519/C64/ladderstep (real: 256.77, user: 241.34, sys: 0.45, mem: 1617000 ko) COQC src/Specific/X25519/C64/ladderstepDisplay > src/Specific/X25519/C64/ladderstepDisplay.log