diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-08 11:08:27 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-08 11:08:45 -0700 |
| commit | 35e7650fbc7ff87e945b7e5f7c06f27dd4bd119b (patch) | |
| tree | b553f055e14b66d5dc6676f8a1ed13920d9d828c | |
| parent | 732e7c1a79d3f76bd50c3ced56510dcb50140a13 (diff) | |
Move FancyMachine from Experiments to Specific
Quoting Andres:
> I am leaning towards putting this in Specifc instead of Experiments -- it
> seems like complete result on its own, these files are unlikely to be reused
> for something else, and I don't think we are expecting to need to remove it
> any time soon. Currently, `Specific` code does not quantify over anything (no
> context variables), but this seems secondary. We could make versions of this
> with the curve constants plugged in, though.
| -rw-r--r-- | _CoqProject | 6 | ||||
| -rw-r--r-- | src/Specific/FancyMachine256/Barrett.v (renamed from src/Experiments/FancyMachineBarrett256.v) | 2 | ||||
| -rw-r--r-- | src/Specific/FancyMachine256/Core.v (renamed from src/Experiments/FancyMachine256.v) | 0 | ||||
| -rw-r--r-- | src/Specific/FancyMachine256/Montgomery.v (renamed from src/Experiments/FancyMachineMontgomery256.v) | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/_CoqProject b/_CoqProject index 6bc64c8a4..6cbebb799 100644 --- a/_CoqProject +++ b/_CoqProject @@ -37,9 +37,6 @@ src/Encoding/ModularWordEncodingTheorems.v src/Encoding/PointEncodingPre.v src/Experiments/DerivationsOptionRectLetInEncoding.v src/Experiments/EdDSARefinement.v -src/Experiments/FancyMachine256.v -src/Experiments/FancyMachineBarrett256.v -src/Experiments/FancyMachineMontgomery256.v src/Experiments/GenericFieldPow.v src/Experiments/SpecEd25519.v src/Experiments/SpecificCurve25519.v @@ -85,6 +82,9 @@ src/Spec/ModularWordEncoding.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v +src/Specific/FancyMachine256/Barrett.v +src/Specific/FancyMachine256/Core.v +src/Specific/FancyMachine256/Montgomery.v src/Tactics/VerdiTactics.v src/Tactics/Algebra_syntax/Nsatz.v src/Util/AdditionChainExponentiation.v diff --git a/src/Experiments/FancyMachineBarrett256.v b/src/Specific/FancyMachine256/Barrett.v index 0243c284f..1683522e3 100644 --- a/src/Experiments/FancyMachineBarrett256.v +++ b/src/Specific/FancyMachine256/Barrett.v @@ -1,4 +1,4 @@ -Require Import Crypto.Experiments.FancyMachine256. +Require Import Crypto.Specific.FancyMachine256.Core. Require Import Crypto.ModularArithmetic.BarrettReduction.ZBounded. Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook. diff --git a/src/Experiments/FancyMachine256.v b/src/Specific/FancyMachine256/Core.v index d11cfe6ad..d11cfe6ad 100644 --- a/src/Experiments/FancyMachine256.v +++ b/src/Specific/FancyMachine256/Core.v diff --git a/src/Experiments/FancyMachineMontgomery256.v b/src/Specific/FancyMachine256/Montgomery.v index 0f8d8bd59..a9a50f773 100644 --- a/src/Experiments/FancyMachineMontgomery256.v +++ b/src/Specific/FancyMachine256/Montgomery.v @@ -1,4 +1,4 @@ -Require Import Crypto.Experiments.FancyMachine256. +Require Import Crypto.Specific.FancyMachine256.Core. Require Import Crypto.ModularArithmetic.Montgomery.ZBounded. Require Import Crypto.ModularArithmetic.Montgomery.ZProofs. |