diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-30 01:05:10 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-30 01:05:10 -0400 |
| commit | 2722c6d9b9ee60f01eda70b29ab20785859d385c (patch) | |
| tree | 0f3b6b9a2f6f7ff4e3ee7a8cf661f42be5927224 /src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v | |
| parent | 2876f7c688590a64189f47b439f7edf26c91c5de (diff) | |
Fix misnamed references in Specific/ (broke after saturated arithetic reorg)
Diffstat (limited to 'src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v')
| -rw-r--r-- | src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v index bc14eeaad..6adeac3f9 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v @@ -6,6 +6,8 @@ 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.MontgomeryP256_128. 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. @@ -35,8 +37,8 @@ Section BoundedField25p5. Let feW : Type := tuple (wordT lgbitwidth) sz. Let feBW : Type := BoundedWord sz bitwidth bounds. Let eval : feBW -> Z := - fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }. + 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 := @@ -78,7 +80,7 @@ Section BoundedField25p5. eexists_sig_etransitivity. set (nonzeroZ := proj1_sig nonzero). context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ]. - cbv beta iota delta [nonzero nonzero' proj1_sig Saturated.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. + 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 |