Fight namespace pollution

src/.gitignore → .gitignore

@@ -1,3 +1,5 @@
+.nia.cache
+Makefile.coq
 *.vo
 *.v.d
 *.glob

Makefile

@@ -0,0 +1,16 @@
+.PHONY: coq
+coq: Makefile.coq
+	make -f Makefile.coq
+
+Makefile.coq: Makefile _CoqProject
+	coq_makefile -f _CoqProject  > $@
+
+SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
+.PHONY: update-_CoqProject
+update-_CoqProject::
+	(echo '-R src ""'; (git ls-files 'src/*.v' | $(SORT_COQPROJECT))) > _CoqProject
+
+.PHONY: clean
+clean:
+	make -f Makefile.coq clean || true
+	rm -f Makefile.coq || true

README.md

@@ -1,12 +1,37 @@
-
 Foundational Cryptography Framework for machine-checked proofs of cryptography in the computational model.    
 
-Getting Started:
-1) cd src/FCF
+# Dependencies
+
+Coq 8.6 or 8.5
+
+# Building
 
-2) make
+`make` 
+
+# Exploring 
 
 Then open a simple example from the “src/examples” directory in Proof General.  A good place to start is “ElGamal.v.”  Interactively step through this proof to learn how to develop a simple proof of non-adaptive security in the concrete setting.  PRF_Encryption_IND_CPA.v contains a more complex proof of adaptive security along with a proof in the asymptotic setting.  
 
+
 The publications describing FCF are available at adam.petcher.net.   
 
+# Importing
+
+  env COQPATH=/path/to/fcf/src proofgeneral test.v
+  Require Import FCF.FCF.
+
+# History
+
+This repository used to contain a proof of security of ESPADA SSE Scheme under
+`src/ESPADA`. This proof is no longer maintained; it is preserved in git
+history.
+
+Some files that no longer fully build are preserved under `src/FCF/Broken`.
+There be dragons, though -- not all of them were ever finished, and some contain
+significant `admit`s.
+
+# Ackowledgements
+
+This work is sponsored by the Department of the Air Force under Air Force Contract FA8721-05-C-0002. Opinions, interpretations, conclusions, and recommendations are those of the author and are not necessarily endorsed by the United States Government.
+
+This work is sponsored by the Intelligence Advanced Research Projects Activity under Air Force Contract FA8721-05-C-0002. Opinions, interpretations, conclusions, and recommendations are those of the author and are not necessarily endorsed by the United States Government.

_CoqProject

@@ -0,0 +1,74 @@
+-R src ""
+src/FCF/Admissibility.v
+src/FCF/Array.v
+src/FCF/Asymptotic.v
+src/FCF/Bernoulli.v
+src/FCF/Blist.v
+src/FCF/Class.v
+src/FCF/Comp.v
+src/FCF/CompFold.v
+src/FCF/ConstructedFunc.v
+src/FCF/Crypto.v
+src/FCF/DetSem.v
+src/FCF/DiffieHellman.v
+src/FCF/DistRules.v
+src/FCF/DistSem.v
+src/FCF/DistTacs.v
+src/FCF/Encryption.v
+src/FCF/Encryption_PK.v
+src/FCF/EqDec.v
+src/FCF/ExpectedPolyTime.v
+src/FCF/FCF.v
+src/FCF/Fold.v
+src/FCF/GenTacs.v
+src/FCF/GroupTheory.v
+src/FCF/HasDups.v
+src/FCF/Hybrid.v
+src/FCF/Limit.v
+src/FCF/Lognat.v
+src/FCF/NoDup_gen.v
+src/FCF/NotationV1.v
+src/FCF/NotationV2.v
+src/FCF/OTP.v
+src/FCF/OracleCompFold.v
+src/FCF/OracleHybrid.v
+src/FCF/PRF.v
+src/FCF/PRF_Convert.v
+src/FCF/PRG.v
+src/FCF/PRP_PRF.v
+src/FCF/ProgTacs.v
+src/FCF/ProgramLogic.v
+src/FCF/Rat.v
+src/FCF/RepeatCore.v
+src/FCF/RndDup.v
+src/FCF/RndGrpElem.v
+src/FCF/RndInList.v
+src/FCF/RndListElem.v
+src/FCF/RndNat.v
+src/FCF/RndPerm.v
+src/FCF/SemEquiv.v
+src/FCF/SplitVector.v
+src/FCF/StdNat.v
+src/FCF/Tactics.v
+src/FCF/TwoWorldsEquiv.v
+src/FCF/WC_PolyTime.v
+src/FCF/WC_PolyTime_old.v
+src/FCF/Broken/Encryption_2W.v
+src/FCF/Broken/ListHybrid.v
+src/FCF/Broken/Procedure.v
+src/FCF/Broken/RandPermSwitching.v
+src/FCF/Broken/Sigma.v
+src/FCF/Broken/State.v
+src/FCF/examples/Commit.v
+src/FCF/examples/EC_DRBG.v
+src/FCF/examples/ElGamal.v
+src/FCF/examples/PRF_DRBG.v
+src/FCF/examples/PRF_Encryption_IND_CPA.v
+src/HMAC/GHMAC_PRF.v
+src/HMAC/GNMAC_PRF.v
+src/HMAC/HMAC_PRF.v
+src/HMAC/HMAC_spec.v
+src/HMAC/Message.v
+src/HMAC/NMAC_to_HMAC.v
+src/HMAC/cAU.v
+src/HMAC/hF.v