search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
721 stars 146 forks source link

A Big Rename #14

Closed JasonGross closed 7 years ago

JasonGross commented 8 years ago

Is there any reason that we use CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v rather than CompleteEdwardsCurve/Theorems.v? From my experience with the category theory library in HoTT, managing the complete namespace in each file independently of the directory structure becomes a headache, and can easily lead to inconsistent styling.

andres-erbsen commented 8 years ago

I agree that repeating the directory name in each file name is redundant. The current directory structure outside Spec has not received much thought. Perhaps better names would be Curves/Edwards/Affine.v and Curves/Edwards/Extended.v -- "Theorems" isn't particularly informative in a Coq development either. Generalizing from this a little bit, I think we should mirror EFD's shape/coordinates/formula structure for elliptic curves because (1) the properties we verify mostly match the properties they verify (2) I don't see a problem with EFD's directory structure. It's still unclear how expressive a name should be: CompleteTwistedEdwards vs CompleteEdwards vs TwistedEdwards vs Edwards -- for some reason i included the completeness requirement in the name but omitted the specific curve shape. Including both seems like a slippery slope...

andres-erbsen commented 7 years ago

I think we should do a cleanup/rename pass on the repository, perhaps the next time I feel like doing low-brain work. Here is what I propose:

  1. Keep Spec/ as-is because it is fine
  2. Remove BaseSystem and ModularBaseSystem and their users
  3. Remove Assembly and all of its users
  4. Remove Spec/Encoding
  5. Remove PointEncoding
  6. See whether we still use VerdiTactics, remove it unless we use it heavily
  7. I wouldn't touch Reflection because I don't understand it well enough
  8. Consolidate elliptic curve files to paths like Curves/Weierstrass/Projective.v, Curves/Edwards/Twisted. Spec still stays in spec.
  9. Remove most of Specific, only keep FancyMachine stuff?
  10. Remove SpecificGen
  11. Create a new directory for "BaseSystem" kind of stuff, perhaps "Arithmetic"?
  12. Remove coqprime-8.4? I can't remember the project built on 8.4, so meh, we probably are not going to fix it.
jadephilipoom commented 7 years ago

++

  1. IIRC, break_if requires VerdiTactics, and is used in many places.
  2. Specific contains NewBaseSystemTest, which I'm using. I'd like that to remain (although moving it is fine).
  3. extra ++, I would also like to talk about how to organize the stuff in there so that people other than me understand it.
JasonGross commented 7 years ago

re 6. There's very similar code in Crypto.Util.Tactics.BreakMatch; we should use that instead, or figure out if there's missing functionality

re 7. I'd like to fix that. We should rename SmartMap to something better without Smart, and remove the outdated versions of wordsize selection, at the very least.

re 9. I don't want to remove the reflective stuff in there (or any of its dependencies) until we finish have a working Pipeline file that we can use to reify the various operations. But we can deprecate the directory or something.

re 12. Yes, let's get rid of 8.4 support, so we can start using some of the nicer features of 8.5, like simple refine (which allows transparent assert) and dependent subgoals.

andres-erbsen commented 7 years ago

re 7: I also want to do that, but would rather do it separately from simple rename tasks. re 9: hmm. All of that depends on old BaseSystem I think. So maybe we wait until new basesystem integration even somewhat happens.

andres-erbsen commented 7 years ago
  1. Remove most of extraction-related stuff, perhaps consolidate the reusable parts into a Util file.
JasonGross commented 7 years ago
  1. Remove most of Util.FixedWordSizes, which is only needed if we want separate extraction constants for word32, word64, etc.
andres-erbsen commented 7 years ago
  1. Default to removing all experiments, unless we want to keep some.
andres-erbsen commented 7 years ago

What should we do about BoundedArithmetic and stuff that uses it (e g Specific FancyMachine code)? I didn't realize it depends on old BaseSystem... Do we think there is a significant chance we will resume working on that strategy? I think if we don't plan to work on it, we should remove all FancyMachine stuff from master, and if we ever end up needing it, we can dig it up from git history.

andres-erbsen commented 7 years ago

This is happening.

andres-erbsen commented 7 years ago

I ended up not doing 14.