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 /_CoqProject | |
| 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.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 6 |
1 files changed, 3 insertions, 3 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 |