diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-28 18:40:28 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
| commit | 4964f1ff2d40ba08573deddca56140c4ac4b19eb (patch) | |
| tree | 61b24623e414dfa3e09a32cf62e8acd1909dae37 /src/Specific | |
| parent | fbb0f64892560322ed9dcd0f664e730e74de9b4e (diff) | |
Refactor ModularArithmetic into Zmod, expand Decidable
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF1305.v | 4 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index fba77a4a8..b1500b5c9 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -11,6 +11,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. +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. @@ -35,8 +36,7 @@ Definition mul2modulus : fe1305 := Instance subCoeff : SubtractionCoefficient modulus params1305. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - apply ZToField_eqmod. - cbv; reflexivity. + vm_decide. Defined. Definition freezePreconditions1305 : freezePreconditions params1305 int_width. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 7ece3a5da..b0323c4a0 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -11,6 +11,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. +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. @@ -33,8 +34,7 @@ Definition mul2modulus : fe25519 := Instance subCoeff : SubtractionCoefficient modulus params25519. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - apply ZToField_eqmod. - cbv; reflexivity. + vm_decide. Defined. Definition freezePreconditions25519 : freezePreconditions params25519 int_width. |