blob: 4f2b623e0df34babf807375bd84ec84c6883d54c (
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
|
Require Export Crypto.Spec.ModularArithmetic.
Require Export Coq.setoid_ring.Field.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Local Open Scope F_scope.
Definition OpaqueF := F.
Definition OpaqueZmodulo := BinInt.Z.modulo.
Definition Opaqueadd {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @add p.
Definition Opaquemul {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @mul p.
Definition Opaquesub {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @sub p.
Definition Opaquediv {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @div p.
Definition Opaqueopp {p} : OpaqueF p -> OpaqueF p := @opp p.
Definition Opaqueinv {p} : OpaqueF p -> OpaqueF p := @inv p.
Definition OpaqueZToField {p} : BinInt.Z -> OpaqueF p := @ZToField p.
Definition Opaqueadd_correct {p} : @Opaqueadd p = @add p := eq_refl.
Definition Opaquesub_correct {p} : @Opaquesub p = @sub p := eq_refl.
Definition Opaquemul_correct {p} : @Opaquemul p = @mul p := eq_refl.
Definition Opaquediv_correct {p} : @Opaquediv p = @div p := eq_refl.
Global Opaque F OpaqueZmodulo Opaqueadd Opaquemul Opaquesub Opaquediv Opaqueopp Opaqueinv OpaqueZToField.
Definition OpaqueFieldTheory p {prime_p} : @field_theory (OpaqueF p) (OpaqueZToField 0%Z) (OpaqueZToField 1%Z) Opaqueadd Opaquemul Opaquesub Opaqueopp Opaquediv Opaqueinv eq := Eval hnf in @Ffield_theory p prime_p.
Ltac FIELD_SIMPL_idtac FLD lH rl :=
let Simpl := idtac (* (protect_fv "field") *) in
let lemma := get_SimplifyEqLemma FLD in
get_FldPre FLD ();
Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
get_FldPost FLD ().
Ltac field_simplify_eq_idtac := let G := Get_goal in field_lookup (PackField FIELD_SIMPL_idtac) [] G.
Ltac F_to_Opaque :=
change F with OpaqueF in *;
change BinInt.Z.modulo with OpaqueZmodulo in *;
change @add with @Opaqueadd in *;
change @mul with @Opaquemul in *;
change @sub with @Opaquesub in *;
change @div with @Opaquediv in *;
change @opp with @Opaqueopp in *;
change @inv with @Opaqueinv in *;
change @ZToField with @OpaqueZToField in *.
Ltac F_from_Opaque p :=
change OpaqueF with F in *;
change (@sig BinNums.Z (fun z : BinNums.Z => @eq BinNums.Z z (BinInt.Z.modulo z p))) with (F p) in *;
change OpaqueZmodulo with BinInt.Z.modulo in *;
change @Opaqueopp with @opp in *;
change @Opaqueinv with @inv in *;
change @OpaqueZToField with @ZToField in *;
rewrite ?@Opaqueadd_correct, ?@Opaquesub_correct, ?@Opaquemul_correct, ?@Opaquediv_correct in *.
Ltac F_field_simplify_eq :=
lazymatch goal with |- @eq (F ?p) _ _ =>
F_to_Opaque;
field_simplify_eq_idtac;
compute;
F_from_Opaque p
end.
Ltac F_field := F_field_simplify_eq; [ring|..].
Ltac notConstant t := constr:NotConstant.
|
