blob: f0db6c93796217c3e98d8d32b6380975ea2247ed (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
Require Import Crypto.Specific.X25519.C64.ReificationTypes.
Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
Require Import Crypto.Arithmetic.Core.
Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
(* TODO : change this to field once field isomorphism happens *)
Definition mul :
{ mul : feBW -> feBW -> feBW
| forall a b, phiBW (mul a b) = F.mul (phiBW a) (phiBW b) }.
Proof.
start_preglue.
do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
all:fin_preglue.
(* jgross start here! *)
(*Set Ltac Profiling.*)
Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
(*Show Ltac Profile.*)
(* total time: 19.632s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s
─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s
─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s
─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s
─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s
─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s
─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s
─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s
─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s
─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s
─eexact -------------------------------- 4.1% 4.1% 68 0.028s
─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s
─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s
─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s
─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s
─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s
─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s
─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s
├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s
│└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s
│ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s
│ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s
│ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s
│ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s
│ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s
│ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s
│ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s
│ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s
│ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s
│ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s
│ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s
│ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s
└─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s
*)
Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
|
