diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-05 22:32:49 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
| commit | ffa0731cc244091460586b46bf4817e5a918ba49 (patch) | |
| tree | 05bfc8058a8af3469d3652d8a7b95ca5ab45c37f /src | |
| parent | b6e37eee58b0a8f43711533d49392172786e2cb5 (diff) | |
Reorgainze synthesis framework files into a Framework folder
Diffstat (limited to 'src')
44 files changed, 45 insertions, 45 deletions
diff --git a/src/Specific/ArithmeticSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesisFramework.v index 352ac7d41..77624ed41 100644 --- a/src/Specific/ArithmeticSynthesisFramework.v +++ b/src/Specific/Framework/ArithmeticSynthesisFramework.v @@ -3,7 +3,7 @@ Require Import Coq.Lists.List. Import ListNotations. Require Import Crypto.Arithmetic.Core. Import B. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Arithmetic.Saturated.Freeze. -Require Crypto.Specific.CurveParameters. +Require Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.BreakMatch. diff --git a/src/Specific/CurveParameters.v b/src/Specific/Framework/CurveParameters.v index aa679a4d3..aa679a4d3 100644 --- a/src/Specific/CurveParameters.v +++ b/src/Specific/Framework/CurveParameters.v diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/Framework/IntegrationTestDisplayCommon.v index 6d68da21a..a3bf52d85 100644 --- a/src/Specific/IntegrationTestDisplayCommon.v +++ b/src/Specific/Framework/IntegrationTestDisplayCommon.v @@ -1,14 +1,14 @@ Require Import Crypto.Util.Sigma.Lift. Require Import Crypto.Util.Sigma.Associativity. Require Import Crypto.Util.Sigma.MapProjections. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Eta. Require Export Coq.ZArith.ZArith. Require Export Crypto.Util.LetIn. Require Export Crypto.Util.FixedWordSizes. Require Export Crypto.Compilers.Syntax. -Require Export Crypto.Specific.IntegrationTestDisplayCommonTactics. +Require Export Crypto.Specific.Framework.IntegrationTestDisplayCommonTactics. Require Export Crypto.Compilers.Z.HexNotationConstants. Require Export Crypto.Util.Notations. Require Export Crypto.Compilers.Z.CNotations. diff --git a/src/Specific/IntegrationTestDisplayCommonTactics.v b/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v index 999fbe1ed..2b15616fe 100644 --- a/src/Specific/IntegrationTestDisplayCommonTactics.v +++ b/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v @@ -1,7 +1,7 @@ Require Import Crypto.Util.Sigma.Lift. Require Import Crypto.Util.Sigma.Associativity. Require Import Crypto.Util.Sigma.MapProjections. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Eta. Require Import Coq.ZArith.ZArith. diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v index 41bef884c..41bef884c 100644 --- a/src/Specific/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v diff --git a/src/Specific/LadderstepSynthesisFramework.v b/src/Specific/Framework/LadderstepSynthesisFramework.v index d6afb31eb..d6afb31eb 100644 --- a/src/Specific/LadderstepSynthesisFramework.v +++ b/src/Specific/Framework/LadderstepSynthesisFramework.v diff --git a/src/Specific/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v index 3a160e04d..3a160e04d 100644 --- a/src/Specific/ReificationTypes.v +++ b/src/Specific/Framework/ReificationTypes.v diff --git a/src/Specific/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v index a09e2fd61..c30024181 100644 --- a/src/Specific/SynthesisFramework.v +++ b/src/Specific/Framework/SynthesisFramework.v @@ -1,12 +1,12 @@ -Require Import Crypto.Specific.ArithmeticSynthesisFramework. -Require Import Crypto.Specific.ReificationTypes. -Require Import Crypto.Specific.LadderstepSynthesisFramework. +Require Import Crypto.Specific.Framework.ArithmeticSynthesisFramework. +Require Import Crypto.Specific.Framework.ReificationTypes. +Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Util.BoundedWord. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. -Require Crypto.Specific.CurveParameters. +Require Crypto.Specific.Framework.CurveParameters. Module Export Exports. Export ArithmeticSynthesisFramework.Exports. diff --git a/src/Specific/IntegrationTestFreezeDisplay.v b/src/Specific/IntegrationTestFreezeDisplay.v index c6d13e05a..ab17a7e93 100644 --- a/src/Specific/IntegrationTestFreezeDisplay.v +++ b/src/Specific/IntegrationTestFreezeDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestFreeze. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display freeze. diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v index 0a29973a1..8474a05c9 100644 --- a/src/Specific/IntegrationTestKaratsubaMul.v +++ b/src/Specific/IntegrationTestKaratsubaMul.v @@ -11,7 +11,7 @@ Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.MoveLetIn. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestKaratsubaMulDisplay.v b/src/Specific/IntegrationTestKaratsubaMulDisplay.v index 96312713b..7649ca88b 100644 --- a/src/Specific/IntegrationTestKaratsubaMulDisplay.v +++ b/src/Specific/IntegrationTestKaratsubaMulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestKaratsubaMul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index e97784c5a..aba794f4b 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Curves.Montgomery.XZ. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestLadderstep130Display.v b/src/Specific/IntegrationTestLadderstep130Display.v index 41efe786d..fa498e475 100644 --- a/src/Specific/IntegrationTestLadderstep130Display.v +++ b/src/Specific/IntegrationTestLadderstep130Display.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestLadderstep130. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display xzladderstep. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128.v b/src/Specific/IntegrationTestMontgomeryP256_128.v index feca5ad9a..d2b64d3b9 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.v b/src/Specific/IntegrationTestMontgomeryP256_128Display.v index 6b96923fc..420ff7dc5 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128Display.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128Display.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v index a9fea3ef1..ff94e57ee 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v index dcacc2227..13c7937cb 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Add. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display add. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v index 27e710fe6..76664255c 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v @@ -17,7 +17,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v index 0f9c0c284..0d76f5171 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Nonzero. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display nonzero. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v index 1869a7952..c908c1258 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v index 0abe0f38d..ca8721d7d 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Opp. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display opp. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v index 62b1ef328..8f3df4cdf 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v index 55e6595fe..879a8e0cd 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Sub. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display sub. diff --git a/src/Specific/IntegrationTestSubDisplay.v b/src/Specific/IntegrationTestSubDisplay.v index 9f8e5eadc..37a060f26 100644 --- a/src/Specific/IntegrationTestSubDisplay.v +++ b/src/Specific/IntegrationTestSubDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestSub. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display sub. diff --git a/src/Specific/NISTP256/AMD64/feadd.v b/src/Specific/NISTP256/AMD64/feadd.v index 5de6fc03a..23a38978c 100644 --- a/src/Specific/NISTP256/AMD64/feadd.v +++ b/src/Specific/NISTP256/AMD64/feadd.v @@ -15,7 +15,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/feaddDisplay.v b/src/Specific/NISTP256/AMD64/feaddDisplay.v index 452044402..b6e79f393 100644 --- a/src/Specific/NISTP256/AMD64/feaddDisplay.v +++ b/src/Specific/NISTP256/AMD64/feaddDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.feadd. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display add. diff --git a/src/Specific/NISTP256/AMD64/femul.v b/src/Specific/NISTP256/AMD64/femul.v index f87e6d26b..5904b1fff 100644 --- a/src/Specific/NISTP256/AMD64/femul.v +++ b/src/Specific/NISTP256/AMD64/femul.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/femulDisplay.v b/src/Specific/NISTP256/AMD64/femulDisplay.v index f47c0ba06..acde66b0e 100644 --- a/src/Specific/NISTP256/AMD64/femulDisplay.v +++ b/src/Specific/NISTP256/AMD64/femulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.femul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v index c74e7a872..13dc4478f 100644 --- a/src/Specific/NISTP256/AMD64/fenz.v +++ b/src/Specific/NISTP256/AMD64/fenz.v @@ -17,7 +17,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/fenzDisplay.v b/src/Specific/NISTP256/AMD64/fenzDisplay.v index c4119449f..77c48f76f 100644 --- a/src/Specific/NISTP256/AMD64/fenzDisplay.v +++ b/src/Specific/NISTP256/AMD64/fenzDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.fenz. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display nonzero. diff --git a/src/Specific/NISTP256/AMD64/feopp.v b/src/Specific/NISTP256/AMD64/feopp.v index 14342c238..d57948035 100644 --- a/src/Specific/NISTP256/AMD64/feopp.v +++ b/src/Specific/NISTP256/AMD64/feopp.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/feoppDisplay.v b/src/Specific/NISTP256/AMD64/feoppDisplay.v index 9075af2f2..7d2a65b6f 100644 --- a/src/Specific/NISTP256/AMD64/feoppDisplay.v +++ b/src/Specific/NISTP256/AMD64/feoppDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.feopp. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display opp. diff --git a/src/Specific/NISTP256/AMD64/fesub.v b/src/Specific/NISTP256/AMD64/fesub.v index adf278faa..4098ffcfc 100644 --- a/src/Specific/NISTP256/AMD64/fesub.v +++ b/src/Specific/NISTP256/AMD64/fesub.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/fesubDisplay.v b/src/Specific/NISTP256/AMD64/fesubDisplay.v index 0f771869c..01559b019 100644 --- a/src/Specific/NISTP256/AMD64/fesubDisplay.v +++ b/src/Specific/NISTP256/AMD64/fesubDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.fesub. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display sub. diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v index 8e7848bc1..5040bf182 100644 --- a/src/Specific/X25519/C32/CurveParameters.v +++ b/src/Specific/X25519/C32/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.CurveParameters. +Require Import Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.LetIn. (*** diff --git a/src/Specific/X25519/C32/Synthesis.v b/src/Specific/X25519/C32/Synthesis.v index f4068d043..3b9b35078 100644 --- a/src/Specific/X25519/C32/Synthesis.v +++ b/src/Specific/X25519/C32/Synthesis.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.SynthesisFramework. +Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X25519.C32.CurveParameters. Module Import T := MakeSynthesisTactics Curve. diff --git a/src/Specific/X25519/C32/femulDisplay.v b/src/Specific/X25519/C32/femulDisplay.v index e603a33c0..d37a0e668 100644 --- a/src/Specific/X25519/C32/femulDisplay.v +++ b/src/Specific/X25519/C32/femulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C32.femul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/X25519/C32/fesquareDisplay.v b/src/Specific/X25519/C32/fesquareDisplay.v index 1cc917c7e..5075db1fd 100644 --- a/src/Specific/X25519/C32/fesquareDisplay.v +++ b/src/Specific/X25519/C32/fesquareDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C32.fesquare. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display square. diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 1e15eea24..3b8016e96 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.CurveParameters. +Require Import Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.LetIn. (*** diff --git a/src/Specific/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v index d77bb5cee..3c3bac04d 100644 --- a/src/Specific/X25519/C64/Synthesis.v +++ b/src/Specific/X25519/C64/Synthesis.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.SynthesisFramework. +Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X25519.C64.CurveParameters. Module Import T := MakeSynthesisTactics Curve. diff --git a/src/Specific/X25519/C64/femulDisplay.v b/src/Specific/X25519/C64/femulDisplay.v index 35c557ce5..0e77976ca 100644 --- a/src/Specific/X25519/C64/femulDisplay.v +++ b/src/Specific/X25519/C64/femulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.femul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/X25519/C64/fesquareDisplay.v b/src/Specific/X25519/C64/fesquareDisplay.v index f39710fec..e722863e2 100644 --- a/src/Specific/X25519/C64/fesquareDisplay.v +++ b/src/Specific/X25519/C64/fesquareDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.fesquare. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display square. diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v index 11238e0b2..adb20912e 100644 --- a/src/Specific/X25519/C64/ladderstep.v +++ b/src/Specific/X25519/C64/ladderstep.v @@ -1,6 +1,6 @@ Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.LadderstepSynthesisFramework. +Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. Require Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) diff --git a/src/Specific/X25519/C64/ladderstepDisplay.v b/src/Specific/X25519/C64/ladderstepDisplay.v index 73aab21ab..0716f8ef1 100644 --- a/src/Specific/X25519/C64/ladderstepDisplay.v +++ b/src/Specific/X25519/C64/ladderstepDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.ladderstep. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display xzladderstep. |