blob: cfea6e957584aeecd6d1a6c7e3b2e2216375493c (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Local Open Scope Z_scope.
Require Import Crypto.Arithmetic.Core.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
Require Import Crypto.Arithmetic.Core. Import B.
Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
Require Import Crypto.Arithmetic.Saturated.UniformWeight.
Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
Require Import Crypto.Util.Tactics.Head.
Require Import Crypto.Util.Tactics.MoveLetIn.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Import ListNotations.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
Section BoundedField25p5.
Local Coercion Z.of_nat : nat >-> Z.
Let bound1 : zrange
:= Eval compute in
{| lower := 0 ; upper := r-1 |}.
Let bounds : Tuple.tuple zrange sz
:= Eval compute in
Tuple.repeat bound1 sz.
Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))).
Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
Let feZ : Type := tuple Z sz.
Let feW : Type := tuple (wordT lgbitwidth) sz.
Let feBW : Type := BoundedWord sz bitwidth bounds.
Let eval : feBW -> Z :=
fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
Let phi : feBW -> F m :=
fun x => montgomery_to_F (eval x).
(* TODO : change this to field once field isomorphism happens *)
Definition nonzero
: { nonzero : feBW_small -> BoundedWord 1 bitwidth bound1
| forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }.
Proof.
lazymatch goal with
| [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ]
=> apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a)
end.
intros a.
cbv [feBW_of_feBW_small].
eexists_sig_etransitivity. all:cbv [phi eval].
refine (_ : (if Decidable.dec (_ = 0) then true else false) = _).
lazymatch goal with
| [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ]
=> cut (x <-> y);
[ destruct (Decidable.dec x), (Decidable.dec y); try reflexivity; intros [? ?];
generalize dependent x; generalize dependent y; solve [ intuition congruence ]
| ]
end.
etransitivity; [ | eapply (proj2_sig nonzero) ];
[ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ].
reflexivity.
let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in
apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _).
{ intros a' H'; rewrite H'.
let H := fresh in
lazymatch goal with |- context[Decidable.dec ?x] => destruct (Decidable.dec x) as [H|H]; try rewrite H end.
{ reflexivity. }
{ let H := fresh in
lazymatch goal with |- context[?x =? 0] => destruct (x =? 0) eqn:? end;
try reflexivity.
Z.ltb_to_lt; congruence. } }
eexists_sig_etransitivity.
set (nonzeroZ := proj1_sig nonzero).
context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
reflexivity.
sig_dlet_in_rhs_to_context.
match goal with
| [ H : feBW_small |- _ ] => destruct H as [? _]
end.
(* jgross start here! *)
Set Ltac Profiling.
(* Set Ltac Profiling.
Print Ltac ReflectiveTactics.solve_side_conditions.
Ltac ReflectiveTactics.solve_side_conditions ::= idtac.
Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
{ Time ReflectiveTactics.do_reify. }
{ Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
{ Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
{ Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
{ Require Import CNotations.
Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
{ Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
{ Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
{ Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
{ Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. }
{ Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
{ Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
{ Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
{ Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
{ Time ReflectiveTactics.handle_boundedness_side_condition. } *)
Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
Show Ltac Profile.
Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *)
Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *)
Print Assumptions nonzero.
|
