A Big Rename about fiat-crypto HOT 11 CLOSED

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...

from fiat-crypto.

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.

from fiat-crypto.

++

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

from fiat-crypto.

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.

from fiat-crypto.

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.

from fiat-crypto.

13. Remove most of extraction-related stuff, perhaps consolidate the reusable parts into a Util file.

from fiat-crypto.

14. Remove most of Util.FixedWordSizes, which is only needed if we want separate extraction constants for word32, word64, etc.

from fiat-crypto.

15. Default to removing all experiments, unless we want to keep some.

from fiat-crypto.

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.

from fiat-crypto.

This is happening.

from fiat-crypto.

I ended up not doing 14.

from fiat-crypto.