From 299206fc77217802c4431ccda1a7c0cb372f0b87 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 14 Mar 2019 16:32:51 -0400 Subject: fix imports and qualifiers so everything builds --- src/COperationSpecifications.v | 5 +++- src/PushButtonSynthesis/MontgomeryReduction.v | 2 +- src/PushButtonSynthesis/Primitives.v | 17 +++++++---- src/PushButtonSynthesis/SaturatedSolinas.v | 2 ++ .../SaturatedSolinasReificationCache.v | 1 + src/PushButtonSynthesis/UnsaturatedSolinas.v | 3 ++ .../UnsaturatedSolinasReificationCache.v | 2 ++ src/PushButtonSynthesis/WordByWordMontgomery.v | 33 ++++++++++++---------- .../WordByWordMontgomeryReificationCache.v | 5 +++- src/SlowPrimeSynthesisExamples.v | 1 + 10 files changed, 47 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/COperationSpecifications.v b/src/COperationSpecifications.v index 2137c3f86..2ab1e108f 100644 --- a/src/COperationSpecifications.v +++ b/src/COperationSpecifications.v @@ -2,6 +2,10 @@ (** The specifications for the various operations to be synthesized. *) Require Import Coq.ZArith.ZArith Coq.micromega.Lia. Require Import Coq.Lists.List. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Partition. +Require Import Crypto.Arithmetic.WordByWordMontgomery. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -11,7 +15,6 @@ Require Import Crypto.Util.ListUtil.FoldBool. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Arithmetic.Core. Local Open Scope Z_scope. Local Open Scope bool_scope. (** These Imports are only needed for the ring proof *) diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v index f61ece27c..d784ebc3c 100644 --- a/src/PushButtonSynthesis/MontgomeryReduction.v +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -15,7 +15,7 @@ Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. Require Import Crypto.Language. Require Import Crypto.CStringification. Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Arithmetic.FancyMongomeryReduction. +Require Import Crypto.Arithmetic.MongomeryReduction. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.Fancy.Compiler. diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 70448938e..93c2e4c69 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -20,7 +20,12 @@ Require Import Crypto.Util.Tactics.ConstrFail. Require Import Crypto.LanguageWf. Require Import Crypto.Language. Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Partition. Require Import Crypto.Arithmetic.Primitives. +Require Import Crypto.Arithmetic.WordByWordMontgomery. +Require Import Crypto.Arithmetic.UniformWeight. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. @@ -429,7 +434,7 @@ Module CorrectnessStringification. | eval (weight 8 1) _ ?v => let sv := recurse v 9 in maybe_parenthesize (("bytes_eval " ++ sv)%string) 10 lvl - | UniformWeight.uweight ?machine_wordsize ?v + | uweight ?machine_wordsize ?v => recurse (2^(machine_wordsize * Z.of_nat v)) lvl | weight 8 1 ?i => recurse (2^(8 * Z.of_nat i)) lvl @@ -569,7 +574,7 @@ Module CorrectnessStringification. Ltac stringify ctx correctness fname arg_var_data out_var_data := let G := match goal with |- ?G => G end in let correctness := (eval hnf in correctness) in - let correctness := (eval cbv [Partition.partition Arithmetic.WordByWordMontgomery.valid Arithmetic.WordByWordMontgomery.small] in correctness) in + let correctness := (eval cbv [partition WordByWordMontgomery.valid WordByWordMontgomery.small] in correctness) in let correctness := strip_bounds_info correctness in let arg_var_names := constr:(type.map_for_each_lhs_of_arrow (@ToString.C.OfPHOAS.names_of_var_data) arg_var_data) in let out_var_names := constr:(ToString.C.OfPHOAS.names_of_base_var_data out_var_data) in @@ -739,10 +744,10 @@ Section __. Hint Rewrite eval_select - Arithmetic.mulx_correct - Arithmetic.addcarryx_correct - Arithmetic.subborrowx_correct - Arithmetic.cmovznz_correct + Arithmetic.Primitives.mulx_correct + Arithmetic.Primitives.addcarryx_correct + Arithmetic.Primitives.subborrowx_correct + Arithmetic.Primitives.cmovznz_correct Z.zselect_correct using solve [ auto | congruence | solve_extra_bounds_side_conditions ] : push_eval. diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 162b6a3c0..6794108a1 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -23,6 +23,8 @@ Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.CStringification. Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Saturated. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. diff --git a/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v index 0f811e3cf..3fac0f2c9 100644 --- a/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v +++ b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v @@ -1,6 +1,7 @@ (** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic.ModOps. Require Import Crypto.Arithmetic.Saturated. Require Import Crypto.PushButtonSynthesis.ReificationCache. Local Open Scope Z_scope. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index 509f5cdad..3dfb6bfca 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -25,6 +25,9 @@ Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.CStringification. Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Partition. +Require Import Crypto.Arithmetic.Freeze. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v index 8379838f6..251ebc3e6 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v @@ -2,6 +2,8 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.Freeze. +Require Import Crypto.Arithmetic.ModOps. Require Import Crypto.PushButtonSynthesis.ReificationCache. Local Open Scope Z_scope. diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index 5743d2c6a..ebf250664 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -34,7 +34,11 @@ Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.CStringification. Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Freeze. +Require Import Crypto.Arithmetic.Partition. Require Import Crypto.Arithmetic.WordByWordMontgomery. +Require Import Crypto.Arithmetic.UniformWeight. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. @@ -55,7 +59,7 @@ Import COperationSpecifications.Solinas. Import COperationSpecifications.WordByWordMontgomery. Import Associational Positional. -Import Arithmetic.WordByWordMontgomery. +Import Arithmetic.WordByWordMontgomery.WordByWordMontgomery. Import WordByWordMontgomeryReificationCache.WordByWordMontgomery. @@ -99,9 +103,9 @@ Section __. end. Let n_bytes := bytes_n machine_wordsize 1 n. Let prime_upperbound_list : list Z - := Partition.partition (uweight machine_wordsize) n (s-1). + := partition (uweight machine_wordsize) n (s-1). Let prime_bytes_upperbound_list : list Z - := Partition.partition (weight 8 1) n_bytes (s-1). + := partition (weight 8 1) n_bytes (s-1). Let upperbounds : list Z := prime_upperbound_list. Definition prime_bound : ZRange.type.option.interp (base.type.Z) := Some r[0~>m-1]%zrange. @@ -223,9 +227,8 @@ Section __. { use_curve_good_t. } Qed. - - Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). - Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). + Local Notation valid := (valid machine_wordsize n m). + Local Notation bytes_valid := (WordByWordMontgomery.valid 8 n_bytes m). Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). @@ -654,15 +657,15 @@ Section __. using solve [ eauto using length_of_valid | congruence | solve_extra_bounds_side_conditions ] : push_eval. (* needed for making [autorewrite] fast enough *) Local Opaque - Arithmetic.WordByWordMontgomery.onemod - Arithmetic.WordByWordMontgomery.from_montgomerymod - Arithmetic.WordByWordMontgomery.mulmod - Arithmetic.WordByWordMontgomery.squaremod - Arithmetic.WordByWordMontgomery.encodemod - Arithmetic.WordByWordMontgomery.addmod - Arithmetic.WordByWordMontgomery.submod - Arithmetic.WordByWordMontgomery.oppmod - Arithmetic.WordByWordMontgomery.to_bytesmod. + WordByWordMontgomery.WordByWordMontgomery.onemod + WordByWordMontgomery.WordByWordMontgomery.from_montgomerymod + WordByWordMontgomery.WordByWordMontgomery.mulmod + WordByWordMontgomery.WordByWordMontgomery.squaremod + WordByWordMontgomery.WordByWordMontgomery.encodemod + WordByWordMontgomery.WordByWordMontgomery.addmod + WordByWordMontgomery.WordByWordMontgomery.submod + WordByWordMontgomery.WordByWordMontgomery.oppmod + WordByWordMontgomery.WordByWordMontgomery.to_bytesmod. Hint Unfold eval zeromod onemod : push_eval. Local Ltac prove_correctness op_correct := diff --git a/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v index c43633d2d..0cc09df60 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v +++ b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v @@ -2,6 +2,9 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.Freeze. +Require Import Crypto.Arithmetic.ModOps. Require Import Crypto.Arithmetic.WordByWordMontgomery. Require Import Crypto.Language. Require Import Crypto.PushButtonSynthesis.ReificationCache. @@ -17,7 +20,7 @@ Import Associational Positional. Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) Module Export WordByWordMontgomery. - Import Arithmetic.WordByWordMontgomery. + Import WordByWordMontgomery.WordByWordMontgomery. Definition zeromod bitwidth n m m' := encodemod bitwidth n m m' 0. Definition onemod bitwidth n m m' := encodemod bitwidth n m m' 1. diff --git a/src/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v index 0ba59b405..0e00e87e3 100644 --- a/src/SlowPrimeSynthesisExamples.v +++ b/src/SlowPrimeSynthesisExamples.v @@ -6,6 +6,7 @@ Require Import Coq.derive.Derive. Require Import Coq.Lists.List. Require Import Crypto.Util.ZRange. Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. Require Import Crypto.PushButtonSynthesis.UnsaturatedSolinas. Require Import Crypto.CStringification. Require Import Crypto.BoundsPipeline. -- cgit v1.2.3