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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Local Open Scope Z_scope.
Require Import Crypto.Algebra.
Require Import Crypto.NewBaseSystem.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Specific.NewBaseSystemTest.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
Require Import Crypto.Util.Tactics.Head.
Import ListNotations.
Require Import Crypto.Reflection.Z.Bounds.Pipeline.
Section BoundedField25p5.
Local Coercion Z.of_nat : nat >-> Z.
Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 10)).
Let length_lw := Eval compute in List.length limb_widths.
Local Notation b_of exp := {| lower := 0 ; upper := 2^exp + 2^(exp-3) |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
(* The definition [bounds_exp] is a tuple-version of the
limb-widths, which are the [exp] argument in [b_of] above, i.e.,
the approximate base-2 exponent of the bounds on the limb in that
position. *)
Let bounds_exp : Tuple.tuple Z length_lw
:= Eval compute in
Tuple.from_list length_lw limb_widths eq_refl.
Let bounds : Tuple.tuple zrange length_lw
:= Eval compute in
Tuple.map (fun e => b_of e) bounds_exp.
Let feZ : Type := tuple Z 10.
Let feW : Type := tuple word32 10.
Let feBW : Type := BoundedWord 10 32 bounds.
Let phi : feBW -> F m :=
fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
(** TODO MOVE ME *)
(** The [eexists_sig_etransitivity] tactic takes a goal of the form
[{ a | f a = b }], and splits it into two goals, [?b' = b] and
[{ a | f a = ?b' }], where [?b'] is a fresh evar. *)
Definition sig_eq_trans_exist1 {A B} (f : A -> B)
(b b' : B)
(pf : b' = b)
(y : { a : A | f a = b' })
: { a : A | f a = b }
:= let 'exist a p := y in exist _ a (eq_trans p pf).
Ltac eexists_sig_etransitivity :=
lazymatch goal with
| [ |- { a : ?A | @?f a = ?b } ]
=> let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in
simple refine (lem _ _)
end.
(** TODO MOVE ME *)
(** The [save_state_and_back_to_sig] tactic, invoked as [all:
save_state_and_back_to_sig] or in a pipeline, as [stuff;
save_state_and_back_to_sig], operates on two goals
simultaneously, the first of the form [?y = f (k args)], and the
second of the form [{ a | _ = ?y }] (generally it will be
specifically of the form [{ a | f a = ?y }]), and solves the
first by [reflexivity], and, working under the assumption that
[k] is a context variable in the first goal which is not set in
the second goal, stuffs the head of the [k args] (which should
be a lambda) into a new context variable.
This tactic could presumably be generalized to first revert all
of the context definitions used in [f (k args)], then unify that
with [?y] in a way that preserves the let-ins, and then
introduce any let-ins at the head of [?y] into the context. *)
Ltac save_state_and_back_to_sig :=
[> reflexivity
| lazymatch goal with
| [ |- { a | _ = ?f ?k_args } ]
=> let k := head k_args in
let rexprZ := fresh "rexprZ" in
set (rexprZ := k)
end ].
(* TODO : change this to field once field isomorphism happens *)
Definition add :
{ add : feBW -> feBW -> feBW
| forall a b, phi (add a b) = F.add (phi a) (phi b) }.
Proof.
lazymatch goal with
| [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
=> apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
end.
intros.
eexists_sig_etransitivity. all:cbv [phi].
rewrite <- (proj2_sig add_sig).
symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
set (carry_addZ := fun a b => proj1_sig carry_sig (proj1_sig add_sig a b)).
change (proj1_sig carry_sig (proj1_sig add_sig ?a ?b)) with (carry_addZ a b).
let carry_addZ' := (eval cbv beta iota delta [carry_addZ proj1_sig add_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz] in carry_addZ) in
let carry_addZ'' := fresh carry_addZ in
rename carry_addZ into carry_addZ'';
pose carry_addZ' as carry_addZ;
replace carry_addZ'' with carry_addZ by abstract (cbv beta iota delta [carry_addZ'' proj1_sig add_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; reflexivity);
clear carry_addZ''.
all:save_state_and_back_to_sig.
apply (fun f => proj2_sig_map (fun _ p => f_equal f p)).
(* jgross start here! *)
(*Set Ltac Profiling.*)
Time refine_reflectively. (* 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) *)
End BoundedField25p5.
|
