blob: a7f8e5ee5b1e1edda47a618c6b8cda1b0584804e (
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
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
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.KaratsubaPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.MontgomeryPackage.
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ReificationTypesPackage.
Require Import Crypto.Specific.Framework.MontgomeryReificationTypesPackage.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Arithmetic.Core.
Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Util.TagList.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
Module Export Exports.
Export ArithmeticSynthesis.Defaults.Exports.
Export ArithmeticSynthesis.Freeze.Exports.
End Exports.
(* Alisases for exporting *)
Module Type PrePackage := PrePackage.
Module Tag.
Notation Context := Tag.Context (only parsing).
End Tag.
Module Export MakeSynthesisTactics.
Ltac add_Synthesis_package pkg curve extra_prove_mul_eq extra_prove_square_eq :=
let CP := get_fill_CurveParameters curve in
let P_extra_prove_mul_eq := extra_prove_mul_eq in
let P_extra_prove_square_eq := extra_prove_square_eq in
let pkg := Tag.local_update pkg TAG.CP CP in
let pkg := add_CurveParameters_package pkg in
let pkg := Tag.strip_subst_local pkg in
let pkg := add_Base_package pkg in
let pkg := add_ReificationTypes_package pkg in
let pkg := add_Karatsuba_package pkg in
let pkg := add_Montgomery_package pkg in
let pkg := add_MontgomeryReificationTypes_package pkg in
(* N.B. freeze is a "default" and must come after montgomery, which disables it *)
let pkg := add_Freeze_package pkg in
(* N.B. the Defaults must come after other possible ways of adding the _sig lemmas *)
let pkg := add_Defaults_package pkg P_extra_prove_mul_eq P_extra_prove_square_eq in
(* N.B. Ladderstep must come after Defaults *)
let pkg := add_Ladderstep_package pkg in
pkg.
Ltac get_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq :=
let pkg := constr:(Tag.empty) in
add_Synthesis_package pkg curve extra_prove_mul_eq extra_prove_square_eq.
Ltac make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq :=
let pkg := get_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq in
exact pkg.
End MakeSynthesisTactics.
Module PackageSynthesis (PKG : PrePackage).
Module CP := MakeCurveParametersPackage PKG.
Module BP := MakeBasePackage PKG.
Module DP := MakeDefaultsPackage PKG.
Module RP := MakeReificationTypesPackage PKG.
Module FP := MakeFreezePackage PKG.
Module LP := MakeLadderstepPackage PKG.
Module KP := MakeKaratsubaPackage PKG.
Module MP := MakeMontgomeryPackage PKG.
Module MRP := MakeMontgomeryReificationTypesPackage PKG.
Include CP.
Include BP.
Include DP.
Include RP.
Include FP.
Include LP.
Include KP.
Include MP.
Include MRP.
Ltac synthesize do_rewrite get_op_sig :=
let op_sig := get_op_sig () in
let allowable_bit_widths := get_allowable_bit_widths () in
start_preglue;
[ do_rewrite op_sig; cbv_runtime
| .. ];
fin_preglue;
refine_reflectively_gen allowable_bit_widths default.
Ltac synthesize_with_carry do_rewrite get_op_sig :=
let carry_sig := get_carry_sig () in
synthesize ltac:(fun op_sig => do_rewrite op_sig carry_sig) get_op_sig.
Ltac synthesize_narg get_op_sig :=
synthesize do_rewrite_with_sig get_op_sig.
Ltac synthesize_2arg_with_carry get_op_sig :=
synthesize_with_carry do_rewrite_with_2sig_add_carry get_op_sig.
Ltac synthesize_1arg_with_carry get_op_sig :=
synthesize_with_carry do_rewrite_with_1sig_add_carry get_op_sig.
Ltac synthesize_montgomery get_op_sig get_op_bounded :=
let phi := get_phi1_for_preglue () in
let op_sig := get_op_sig () in
let op_bounded := get_op_bounded () in
let allowable_bit_widths := get_allowable_bit_widths () in
let do_red _ :=
lazymatch (eval cbv [phi] in phi) with
| (fun x => ?montgomery_to_F (?meval (?feBW_of_feBW_small _)))
=> cbv [feBW_of_feBW_small meval]
end in
start_preglue;
do_red ();
[ do_rewrite_with_sig_by op_sig op_sig_side_conditions_t;
cbv_runtime
| .. ];
fin_preglue;
factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t;
refine_reflectively_gen allowable_bit_widths anf.
Ltac synthesize_narg_choice_gen synthesize get_op_sig get_op_bounded :=
let montgomery := get_montgomery () in
lazymatch (eval vm_compute in montgomery) with
| true => synthesize_montgomery get_op_sig get_op_bounded
| false => synthesize get_op_sig
end.
Ltac synthesize_narg_choice get_op_sig get_op_bounded :=
synthesize_narg_choice_gen synthesize_narg get_op_sig get_op_bounded.
Ltac synthesize_2arg_choice_with_carry get_op_sig get_op_bounded :=
synthesize_narg_choice_gen synthesize_2arg_with_carry get_op_sig get_op_bounded.
Ltac synthesize_1arg_choice_with_carry get_op_sig get_op_bounded :=
synthesize_narg_choice_gen synthesize_1arg_with_carry get_op_sig get_op_bounded.
Ltac synthesize_carry_mul _ := synthesize_2arg_choice_with_carry get_mul_sig get_mul_bounded.
Ltac synthesize_carry_add _ := synthesize_2arg_choice_with_carry get_add_sig get_add_bounded.
Ltac synthesize_carry_sub _ := synthesize_2arg_choice_with_carry get_sub_sig get_sub_bounded.
Ltac synthesize_carry_opp _ := synthesize_1arg_choice_with_carry get_opp_sig get_opp_bounded.
Ltac synthesize_carry_square _ := synthesize_1arg_with_carry get_square_sig.
Ltac synthesize_nocarry_mul _ := synthesize_narg_choice get_mul_sig get_mul_bounded.
Ltac synthesize_add _ := synthesize_narg_choice get_add_sig get_add_bounded.
Ltac synthesize_sub _ := synthesize_narg_choice get_sub_sig get_sub_bounded.
Ltac synthesize_opp _ := synthesize_narg_choice get_opp_sig get_opp_bounded.
Ltac synthesize_carry _ := synthesize_narg_choice get_carry_sig get_carry_bounded.
Ltac synthesize_nocarry_square _ := synthesize_narg get_square_sig.
Ltac synthesize_mul _ := synthesize_carry_mul ().
Ltac synthesize_square _ := synthesize_carry_square ().
Ltac synthesize_freeze _ :=
let freeze_sig := get_freeze_sig () in
let feBW_tight_bounded := get_feBW_tight_bounded () in
let freeze_allowable_bit_widths := get_freeze_allowable_bit_widths () in
start_preglue;
[ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_tight_bounded); cbv_runtime
| .. ];
fin_preglue;
refine_reflectively_gen freeze_allowable_bit_widths anf.
Ltac synthesize_xzladderstep _ :=
let Mxzladderstep_sig := get_Mxzladderstep_sig () in
let a24_sig := get_a24_sig () in
let allowable_bit_widths := get_allowable_bit_widths () in
start_preglue;
[ unmap_map_tuple ();
do_rewrite_with_sig_1arg Mxzladderstep_sig;
cbv [Mxzladderstep XZ.M.xzladderstep a24_sig]; cbn [proj1_sig];
do_set_sigs ();
cbv_runtime
| .. ];
finish_conjoined_preglue ();
refine_reflectively_gen allowable_bit_widths default.
Ltac synthesize_nonzero _ :=
let op_sig := get_nonzero_sig () in
let allowable_bit_widths := get_allowable_bit_widths () in
nonzero_preglue op_sig ltac:(fun _ => cbv_runtime);
refine_reflectively_gen allowable_bit_widths anf.
End PackageSynthesis.
|
