diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-11 16:32:41 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:03 -0400 |
| commit | 15978c2ec1dea0ee4c1a84d8d56409b575af52cc (patch) | |
| tree | bcd7c1cd23ac35a001774782cf981f4f0caef590 /_CoqProject | |
| parent | 0a8df431e015d70695c6a8d0c5fb73937d9db89f (diff) | |
Define F m, a replacement for GF with several benefits.
- F has a human readable complete specification
- F is a parametric type, not a parametric module
- Different F instances can be disambiguated by type inference,
which is more conventient that notation scopes.
- F has significant support for non-prime moduli
- It should be relatively easy to port existing GF code to F.
Since the repository currently contains code referencing both F and GF,
it makes sense to keep the names different for now. Later, F may or may
not be renamed to GF.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 55b29744f..c1e10953f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,5 @@ -R src Crypto +src/CompleteEwardsCurve/Pre.v src/Curves/PointFormats.v src/Curves/ScalarMult.v src/Galois/BaseSystem.v @@ -9,8 +10,15 @@ src/Galois/GaloisRep.v src/Galois/GaloisTheory.v src/Galois/GaloisTutorial.v src/Galois/ModularBaseSystem.v +src/Galois/ModularBaseSystem.v +src/ModularArithmetic/ModularArithmeticTheorems.v +src/ModularArithmetic/Pre.v +src/ModularArithmetic/PrimeFieldTheorems.v +src/ModularArithmetic/Tutorial.v src/Rep/ECRep.v src/Rep/GaloisRep.v +src/Spec/CompleteEwardsCurve.v +src/Spec/ModularArithmetic.v src/Specific/EdDSA25519.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v |