Merge pull request #1036 from GaloisInc/merge-saw-core-coq

Merge saw-core-coq repository into saw-core.
GaloisInc · Jan 22, 2021 · 89c562b · 89c562b
2 parents 0a6c186 + f3e2782
commit 89c562b
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 6 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -46,9 +46,6 @@
 [submodule "deps/what4"]
 	path = deps/what4
 	url = https://github.com/GaloisInc/what4.git
-[submodule "deps/saw-core-coq"]
-	path = deps/saw-core-coq
-	url = https://github.com/GaloisInc/saw-core-coq.git
 [submodule "deps/argo"]
 	path = deps/argo
 	url = https://github.com/galoisinc/argo
diff --git a/cabal.project b/cabal.project
@@ -13,7 +13,7 @@ packages:
     deps/saw-core/saw-core-aig
     deps/saw-core/saw-core-sbv
     deps/saw-core/saw-core-what4
-    deps/saw-core-coq
+    deps/saw-core/saw-core-coq
     deps/jvm-verifier
     deps/what4/what4
     deps/crucible/crucible

diff --git a/deps/saw-core b/deps/saw-core
diff --git a/deps/saw-core-coq b/deps/saw-core-coq
+5 −0		saw-core-coq/.gitignore
+30 −0		saw-core-coq/LICENSE
+130 −0		saw-core-coq/README.md
+8 −0		saw-core-coq/coq/.gitignore
+13 −0		saw-core-coq/coq/Makefile
+39 −0		saw-core-coq/coq/_CoqProject
+153 −0		saw-core-coq/coq/generated/CryptolToCoq/CryptolPrelude.v
+730 −0		saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
+849 −0		saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+51 −0		saw-core-coq/coq/generated/MEE_CBC.v
+221 −0		saw-core-coq/coq/generated/S2N/LICENSE
+2 −0		saw-core-coq/coq/generated/S2N/NOTICE
+11 −0		saw-core-coq/coq/generated/S2N/README
+2,698 −0		saw-core-coq/coq/generated/S2N/S2N.v
+925 −0		saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v
+548 −0		saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
+512 −0		saw-core-coq/coq/handwritten/CryptolToCoq/CompM_ITrees.v
+27 −0		saw-core-coq/coq/handwritten/CryptolToCoq/CoqVectorsExtra.v
+107 −0		saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
+311 −0		saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
+61 −0		saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
+168 −0		saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePrelude_proofs.v
+301 −0		saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v
+178 −0		saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffoldingCopy.v
+87 −0		saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqLists.v
+355 −0		saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+309 −0		saw-core-coq/coq/handwritten/Lift/Connection.v
+115 −0		saw-core-coq/coq/handwritten/Lift/Handshake.v
+496 −0		saw-core-coq/coq/handwritten/Lift/HandshakeAction.v
+167 −0		saw-core-coq/coq/handwritten/Lift/Minimal.v
+113 −0		saw-core-coq/coq/handwritten/Lift/S2N.v
+50 −0		saw-core-coq/coq/handwritten/Lift/SAWCorePrelude.v
+655 −0		saw-core-coq/coq/handwritten/MEE_CBC_proofs.v
+349 −0		saw-core-coq/coq/handwritten/S2N/Embedding.v
+45 −0		saw-core-coq/coq/handwritten/S2N/Pointed.v
+973 −0		saw-core-coq/coq/handwritten/S2N/S2N_proofs.v
+99 −0		saw-core-coq/coq/handwritten/S2N/Translation/Connection.v
+45 −0		saw-core-coq/coq/handwritten/S2N/Translation/Handshake.v
+50 −0		saw-core-coq/coq/handwritten/S2N/Translation/HandshakeAction.v
+71 −0		saw-core-coq/cryptol/HMAC.cry
+66 −0		saw-core-coq/cryptol/MEE_CBC.cry
+188 −0		saw-core-coq/cryptol/SHA256.cry
+41 −0		saw-core-coq/saw-core-coq.cabal
+2 −0		saw-core-coq/saw/generate_MEE_CBC.saw
+3 −0		saw-core-coq/saw/generate_scaffolding.saw
+75 −0		saw-core-coq/src/Language/Coq/AST.hs
+189 −0		saw-core-coq/src/Language/Coq/Pretty.hs
+146 −0		saw-core-coq/src/Verifier/SAW/Translation/Coq.hs
+43 −0		saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs
+91 −0		saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs
+183 −0		saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs
+486 −0		saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+587 −0		saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+134 −0		saw-core-coq/test/Verifier/SAW/Translation/Coq/Test.hs