blob: 782b89563bfb6e1ee270a0d0b794a2219c18f421 (
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
|
Require Import Crypto.BaseSystem.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
Require Import Crypto.ModularArithmetic.ModularBaseSystem.
Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
Require Export Crypto.Specific.GF25519.
Require Import Crypto.Specific.GF25519BoundedCommon.
Require Import Crypto.Reflection.Reify.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Map.
Require Import Crypto.Reflection.Z.Interpretations64.
Require Crypto.Reflection.Z.Interpretations64.Relations.
Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
Require Import Crypto.Reflection.Z.Reify.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Specific.GF25519Reflective.Common.
Require Import Crypto.Specific.GF25519Reflective.Reified.
Require Import Bedrock.Word Crypto.Util.WordUtil.
Require Import Coq.Lists.List Crypto.Util.ListUtil.
Require Import Crypto.Tactics.VerdiTactics.
Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Algebra.
Import ListNotations.
Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
Local Open Scope Z.
Definition radd : ExprBinOp := Eval vm_compute in rcarry_addW.
Definition rsub : ExprBinOp := Eval vm_compute in rcarry_subW.
Definition rmul : ExprBinOp := Eval vm_compute in rmulW.
Definition ropp : ExprUnOp := Eval vm_compute in rcarry_oppW.
Definition rprefreeze : ExprUnOp := Eval vm_compute in rprefreezeW.
Definition rge_modulus : ExprUnOpFEToZ := Eval vm_compute in rge_modulusW.
Definition rpack : ExprUnOpFEToWire := Eval vm_compute in rpackW.
Definition runpack : ExprUnOpWireToFE := Eval vm_compute in runpackW.
Declare Reduction asm_interp
:= cbv beta iota delta
[id
interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
Eta.interp_flat_type_eta Eta.interp_flat_type_eta_gen
radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W
WordW.interp_op WordW.interp_base_type
Z.interp_op Z.interp_base_type
Z.Syntax.interp_op Z.Syntax.interp_base_type
mapf_interp_flat_type WordW.interp_base_type word64ize
Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
Ltac asm_interp
:= cbv beta iota delta
[id
interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
Eta.interp_flat_type_eta Eta.interp_flat_type_eta_gen
radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W
WordW.interp_op WordW.interp_base_type
Z.interp_op Z.interp_base_type
Z.Syntax.interp_op Z.Syntax.interp_base_type
mapf_interp_flat_type WordW.interp_base_type word64ize
Interp interp interp_flat_type interpf interp_flat_type fst snd].
Definition interp_radd : Specific.GF25519BoundedCommon.fe25519W * Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= Eval asm_interp in interp_bexpr radd.
(*Print interp_radd.*)
Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
Definition interp_rsub : Specific.GF25519BoundedCommon.fe25519W * Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= Eval asm_interp in interp_bexpr rsub.
(*Print interp_rsub.*)
Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
Definition interp_rmul : Specific.GF25519BoundedCommon.fe25519W * Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= Eval asm_interp in interp_bexpr rmul.
(*Print interp_rmul.*)
Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= Eval asm_interp in interp_uexpr ropp.
(*Print interp_ropp.*)
Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
Definition interp_rprefreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
:= Eval asm_interp in interp_uexpr rprefreeze.
(*Print interp_rprefreeze.*)
Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl.
Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
:= Eval asm_interp in interp_uexpr_FEToZ rge_modulus.
Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl.
Definition interp_rpack : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
:= Eval asm_interp in interp_uexpr_FEToWire rpack.
Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl.
Definition interp_runpack : Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
:= Eval asm_interp in interp_uexpr_WireToFE runpack.
Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl.
Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add.
Proof. exact rcarry_addW_correct_and_bounded. Qed.
Lemma rsub_correct_and_bounded : binop_correct_and_bounded rsub carry_sub.
Proof. exact rcarry_subW_correct_and_bounded. Qed.
Lemma rmul_correct_and_bounded : binop_correct_and_bounded rmul mul.
Proof. exact rmulW_correct_and_bounded. Qed.
Lemma ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp.
Proof. exact rcarry_oppW_correct_and_bounded. Qed.
Lemma rprefreeze_correct_and_bounded : unop_correct_and_bounded rprefreeze prefreeze.
Proof. exact rprefreezeW_correct_and_bounded. Qed.
Lemma rge_modulus_correct_and_bounded : unop_FEToZ_correct rge_modulus ge_modulus.
Proof. exact rge_modulusW_correct_and_bounded. Qed.
Lemma rpack_correct_and_bounded : unop_FEToWire_correct_and_bounded rpack pack.
Proof. exact rpackW_correct_and_bounded. Qed.
Lemma runpack_correct_and_bounded : unop_WireToFE_correct_and_bounded runpack unpack.
Proof. exact runpackW_correct_and_bounded. Qed.
|
