aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar jadep <jadep@mit.edu>2019-03-14 16:32:51 -0400
committerGravatar jadephilipoom <jade.philipoom@gmail.com>2019-04-03 23:34:53 +0100
commit299206fc77217802c4431ccda1a7c0cb372f0b87 (patch)
tree80975ef89fbbac45cd9c61277eae73b1c3c6eb1a /src
parenta189b8ad9943cec026ea2797789d8dc72a6d3336 (diff)
fix imports and qualifiers so everything builds
Diffstat (limited to 'src')
-rw-r--r--src/COperationSpecifications.v5
-rw-r--r--src/PushButtonSynthesis/MontgomeryReduction.v2
-rw-r--r--src/PushButtonSynthesis/Primitives.v17
-rw-r--r--src/PushButtonSynthesis/SaturatedSolinas.v2
-rw-r--r--src/PushButtonSynthesis/SaturatedSolinasReificationCache.v1
-rw-r--r--src/PushButtonSynthesis/UnsaturatedSolinas.v3
-rw-r--r--src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v2
-rw-r--r--src/PushButtonSynthesis/WordByWordMontgomery.v33
-rw-r--r--src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v5
-rw-r--r--src/SlowPrimeSynthesisExamples.v1
10 files changed, 47 insertions, 24 deletions
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.