blob: 01f91731e871e5af65135a75262d6cd27075a048 (
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
|
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 MakeSynthesisTactics (Curve : CurveParameters.CurveParameters).
Module P := FillCurveParameters Curve.
Ltac add_Synthesis_package pkg :=
let P_default_mul _ := P.default_mul in
let P_extra_prove_mul_eq _ := P.extra_prove_mul_eq in
let P_default_square _ := P.default_square in
let P_extra_prove_square_eq _ := P.extra_prove_square_eq in
let pkg := P.add_CurveParameters_package 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_default_mul P_extra_prove_mul_eq P_default_square 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 _ :=
let pkg := constr:(Tag.empty) in
add_Synthesis_package pkg.
Ltac make_Synthesis_package _ :=
let pkg := get_Synthesis_package () in
exact pkg.
End MakeSynthesisTactics.
Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePackage).
Module P := CurveParameters.FillCurveParameters Curve.
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_with_carry do_rewrite get_op_sig :=
let carry_sig := get_carry_sig () in
let op_sig := get_op_sig () in
start_preglue;
[ do_rewrite op_sig carry_sig; cbv_runtime
| .. ];
fin_preglue;
refine_reflectively_gen P.allowable_bit_widths default.
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_phi_for_preglue () in
let op_sig := get_op_sig () in
let op_bounded := get_op_bounded () 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 P.allowable_bit_widths anf.
Ltac synthesize_2arg_choice get_op_sig get_op_bounded :=
lazymatch (eval vm_compute in P.montgomery) with
| true => synthesize_montgomery get_op_sig get_op_bounded
| false => synthesize_2arg_with_carry get_op_sig
end.
Ltac synthesize_1arg_choice get_op_sig get_op_bounded :=
lazymatch (eval vm_compute in P.montgomery) with
| true => synthesize_montgomery get_op_sig get_op_bounded
| false => synthesize_1arg_with_carry get_op_sig
end.
Ltac synthesize_mul _ := synthesize_2arg_choice get_mul_sig get_mul_bounded.
Ltac synthesize_add _ := synthesize_2arg_choice get_add_sig get_add_bounded.
Ltac synthesize_sub _ := synthesize_2arg_choice get_sub_sig get_sub_bounded.
Ltac synthesize_opp _ := synthesize_1arg_choice get_opp_sig get_opp_bounded.
Ltac synthesize_square _ := synthesize_1arg_with_carry get_square_sig.
Ltac synthesize_freeze _ :=
let freeze_sig := get_freeze_sig () in
let feBW_bounded := get_feBW_bounded () in
start_preglue;
[ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime
| .. ];
fin_preglue;
refine_reflectively_gen P.freeze_allowable_bit_widths anf.
Ltac synthesize_xzladderstep _ :=
let Mxzladderstep_sig := get_Mxzladderstep_sig () in
let a24_sig := get_a24_sig () 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 P.allowable_bit_widths default.
Ltac synthesize_nonzero _ :=
let op_sig := get_nonzero_sig () in
nonzero_preglue op_sig ltac:(fun _ => cbv_runtime);
refine_reflectively_gen P.allowable_bit_widths anf.
End PackageSynthesis.
|
