blob: 8df44742e94c5032ba548e5661a35a68120a2e60 (
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
|
Require Export Coq.ZArith.ZArith.
Require Export Coq.Strings.String.
Require Export Crypto.Specific.GF25519.
Require Import Crypto.Specific.GF25519BoundedCommon.
Require Import Crypto.Reflection.Reify.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Z.Interpretations.
Require Import Crypto.Reflection.Z.Reify.
Require Export Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.InterpWfRel.
Require Import Crypto.Reflection.Application.
Require Import Crypto.Reflection.MapInterp.
Require Import Crypto.Reflection.MapInterpWf.
Require Import Crypto.Reflection.WfReflective.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.Notations.
Notation Expr := (Expr base_type Word64.interp_base_type op).
Local Ltac make_type_from uncurried_op :=
let T := (type of uncurried_op) in
let T := (eval compute in T) in
let rT := reify_type T in
exact rT.
Definition ExprBinOpT : type base_type.
Proof. make_type_from (uncurry_binop_fe25519 carry_add). Defined.
Definition ExprUnOpT : type base_type.
Proof. make_type_from (uncurry_unop_fe25519 carry_opp). Defined.
Definition ExprUnOpFEToZT : type base_type.
Proof. make_type_from (uncurry_unop_fe25519 ge_modulus). Defined.
Definition ExprUnOpWireToFET : type base_type.
Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
Definition ExprUnOpFEToWireT : type base_type.
Proof. make_type_from (uncurry_unop_fe25519 pack). Defined.
Definition ExprBinOp : Type := Expr ExprBinOpT.
Definition ExprUnOp : Type := Expr ExprUnOpT.
Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
Local Ltac bounds_from_list ls :=
lazymatch (eval hnf in ls) with
| (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |})
| (?x :: ?xs)%list => let bs := bounds_from_list xs in
constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs))
end.
Local Ltac make_bounds ls :=
compute;
let v := bounds_from_list ls in
let v := (eval compute in v) in
exact v.
Definition ExprBinOp_bounds : all_binders_for ExprBinOpT ZBounds.interp_base_type.
Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
Definition ExprUnOp_bounds : all_binders_for ExprUnOpT ZBounds.interp_base_type.
Proof. make_bounds (Tuple.to_list _ bounds). Defined.
Definition ExprUnOpFEToZ_bounds : all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type.
Proof. make_bounds (Tuple.to_list _ bounds). Defined.
Definition ExprUnOpFEToWire_bounds : all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type.
Proof. make_bounds (Tuple.to_list _ bounds). Defined.
Definition ExprUnOpWireToFE_bounds : all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= fun e => curry_binop_fe25519W (Interp (@Word64.interp_op) e).
Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
:= fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
:= fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
:= fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
Notation binop_correct_and_bounded rop op
:= (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
Notation unop_correct_and_bounded rop op
:= (iunop_correct_and_bounded (interp_uexpr rop) op) (only parsing).
Notation unop_FEToZ_correct rop op
:= (iunop_FEToZ_correct (interp_uexpr_FEToZ rop) op) (only parsing).
Notation unop_FEToWire_correct_and_bounded rop op
:= (iunop_FEToWire_correct_and_bounded (interp_uexpr_FEToWire rop) op) (only parsing).
Notation unop_WireToFE_correct_and_bounded rop op
:= (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
Ltac rexpr_cbv :=
lazymatch goal with
| [ |- { rexpr | interp_type_gen_rel_pointwise _ (Interp _ (t:=?T) rexpr) (?uncurry ?oper) } ]
=> let operf := head oper in
let uncurryf := head uncurry in
try cbv delta [T]; try cbv delta [oper];
try cbv beta iota delta [uncurryf]
end;
cbv beta iota delta [interp_flat_type Z.interp_base_type interp_base_type zero_].
Ltac reify_sig :=
rexpr_cbv; eexists; Reify_rhs; reflexivity.
Local Notation rexpr_sig T uncurried_op :=
{ rexprZ
| interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op }
(only parsing).
Notation rexpr_binop_sig op := (rexpr_sig ExprBinOpT (uncurry_binop_fe25519 op)) (only parsing).
Notation rexpr_unop_sig op := (rexpr_sig ExprUnOpT (uncurry_unop_fe25519 op)) (only parsing).
Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25519 op)) (only parsing).
Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe25519 op)) (only parsing).
Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing).
Notation correct_and_bounded_genT ropW'v ropZ_sigv
:= (let ropW' := ropW'v in
let ropZ_sig := ropZ_sigv in
let ropW := MapInterp (fun _ x => x) ropW' in
let ropZ := MapInterp Word64.to_Z ropW' in
let ropBounds := MapInterp ZBounds.of_word64 ropW' in
let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in
ropZ = proj1_sig ropZ_sig
/\ interp_type_rel_pointwise2 Relations.related_Zi (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ)
/\ interp_type_rel_pointwise2 Relations.related_boundsi (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds)
/\ interp_type_rel_pointwise2 Relations.related_word64i (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
(only parsing).
Ltac rexpr_correct :=
let ropW' := fresh in
let ropZ_sig := fresh in
intros ropW' ropZ_sig;
let wf_ropW := fresh "wf_ropW" in
assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl);
cbv zeta; repeat apply conj;
[ vm_compute; reflexivity
| apply @InterpRelWf;
[ | apply @RelWfMapInterp, wf_ropW ].. ];
auto with interp_related.
Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing).
Notation compute_bounds opW bounds
:= (ApplyInterped (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds)
(only parsing).
Module Export PrettyPrinting.
Inductive bounds_on := overflow | in_range (lower upper : Z).
Definition ZBounds_to_bounds_on
:= fun t : base_type
=> match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with
| TZ => fun x => match x with
| Some {| ZBounds.lower := l ; ZBounds.upper := u |}
=> in_range l u
| None
=> overflow
end
end.
(** This gives a slightly easier to read version of the bounds *)
Notation compute_bounds_for_display opW bounds
:= (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds)) (only parsing).
End PrettyPrinting.
|
