Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merge cryptol-verifier into saw-core repository. #805

Merged
merged 1 commit into from
Aug 7, 2020
Merged

Merge cryptol-verifier into saw-core repository. #805

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 0 additions & 3 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,6 @@
[submodule "deps/crucible"]
path = deps/crucible
url = https://github.com/GaloisInc/crucible.git
[submodule "deps/cryptol-verifier"]
path = deps/cryptol-verifier
url = https://github.com/GaloisInc/cryptol-verifier.git
[submodule "deps/cryptol"]
path = deps/cryptol
url = https://github.com/GaloisInc/cryptol.git
Expand Down
1 change: 0 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,6 @@ downloaded dependencies include:
* `deps/abcBridge/`: [Haskell bindings for ABC](https://github.com/GaloisInc/abcBridge)
* `deps/crucible/`: [Crucible symbolic execution engine](https://github.com/GaloisInc/crucible)
* `deps/cryptol/`: [Cryptol](https://github.com/GaloisInc/cryptol)
* `deps/cryptol-verifier/`: [Cryptol Symbolic Simulator (CSS)](https://github.com/GaloisInc/cryptol-verifier)
* `deps/jvm-verifier/`: [Java Symbolic Simulator (JSS)](https://github.com/GaloisInc/jvm-verifier)
* `deps/saw-core/`: [SAWCore intermediate language](https://github.com/GaloisInc/saw-core), used by CSS, JSS, and SAWScript

Expand Down
2 changes: 1 addition & 1 deletion cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,12 @@ packages:
deps/aig
deps/abcBridge
deps/cryptol
deps/saw-core/cryptol-saw-core
deps/saw-core/saw-core
deps/saw-core/saw-core-aig
deps/saw-core/saw-core-sbv
deps/saw-core/saw-core-what4
deps/saw-core-coq
deps/cryptol-verifier
deps/jvm-verifier
deps/what4/what4
deps/what4/what4-abc
Expand Down
2 changes: 1 addition & 1 deletion cabal.project.ci
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,12 @@ packages:
deps/aig
deps/abcBridge
deps/cryptol
deps/saw-core/cryptol-saw-core
deps/saw-core/saw-core
deps/saw-core/saw-core-aig
deps/saw-core/saw-core-sbv
deps/saw-core/saw-core-what4
deps/saw-core-coq
deps/cryptol-verifier
deps/jvm-verifier
deps/what4/what4
deps/what4/what4-abc
Expand Down
2 changes: 1 addition & 1 deletion cabal.project.freeze
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ constraints: any.Cabal ==2.4.0.1,
crucible +unsafe-operations,
any.cryptohash-sha1 ==0.11.100.1,
cryptol +relocatable -static,
cryptol-verifier +build-css,
cryptol-saw-core +build-css,
any.data-accessor ==0.2.3,
data-accessor +category -monadfail +splitbase,
any.data-binary-ieee754 ==0.4.4,
Expand Down
1 change: 0 additions & 1 deletion deps/cryptol-verifier
Open in desktop
Submodule cryptol-verifier deleted from 5fed6d
2 changes: 1 addition & 1 deletion deps/jvm-verifier
Open in desktop
Submodule jvm-verifier updated 1 files
+1 −1 jvm-verifier.cabal
2 changes: 1 addition & 1 deletion deps/saw-core
Open in desktop
Submodule saw-core updated 16 files
+2 −0 .gitignore
+30 −0 cryptol-saw-core/LICENSE
+5 −0 cryptol-saw-core/README.md
+2 −0 cryptol-saw-core/Setup.hs
+93 −0 cryptol-saw-core/cryptol-saw-core.cabal
+138 −0 cryptol-saw-core/css/Main.hs
+1,574 −0 cryptol-saw-core/saw/Cryptol.sawcore
+1,555 −0 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+24 −0 cryptol-saw-core/src/Verifier/SAW/Cryptol/Panic.hs
+22 −0 cryptol-saw-core/src/Verifier/SAW/Cryptol/Prelude.hs
+54 −0 cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs
+598 −0 cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
+61 −0 cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+55 −0 cryptol-saw-core/test/CryptolVerifierTC.hs
+355 −0 cryptol-saw-core/test/instance.cry
+32 −0 cryptol-saw-core/test/superclass.cry
2 changes: 1 addition & 1 deletion deps/saw-core-coq
Open in desktop
Submodule saw-core-coq updated 2 files
+1 −1 README.md
+1 −1 saw-core-coq.cabal
4 changes: 2 additions & 2 deletions saw-script.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ library
, containers
, constraints >= 0.6
, cryptol
, cryptol-verifier
, cryptol-saw-core
, crucible >= 0.4
, crucible-jvm
, crucible-llvm >= 0.2
Expand Down Expand Up @@ -213,4 +213,4 @@ executable saw
, transformers
, saw-script
, saw-core
, cryptol-verifier
, cryptol-saw-core
2 changes: 1 addition & 1 deletion src/SAWScript/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ import Verifier.SAW.TypedAST

import SAWScript.Position

-- cryptol-verifier
-- cryptol-saw-core
import qualified Verifier.SAW.CryptolEnv as CEnv

-- saw-core-aig
Expand Down
2 changes: 1 addition & 1 deletion src/SAWScript/Crucible/JVM/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ import qualified Verifier.Java.Codebase as CB
-- cryptol
import qualified Cryptol.TypeCheck.Type as Cryptol

-- cryptol-verifier
-- cryptol-saw-core
import Verifier.SAW.Cryptol (importType, emptyEnv)

-- what4
Expand Down
2 changes: 1 addition & 1 deletion src/SAWScript/Crucible/JVM/BuiltinsJVM.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ import qualified What4.Solver.Yices as Yices
-- saw-core
import Verifier.SAW.SharedTerm(Term, SharedContext, mkSharedContext, scImplies, scAbstractExts)

-- cryptol-verifier
-- cryptol-saw-core
import Verifier.SAW.TypedTerm(TypedTerm(..))

-- saw-script
Expand Down
2 changes: 1 addition & 1 deletion src/SAWScript/Crucible/LLVM/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedAST
import Verifier.SAW.Recognizer

-- cryptol-verifier
-- cryptol-saw-core
import Verifier.SAW.TypedTerm

-- saw-script
Expand Down
2 changes: 1 addition & 1 deletion src/SAWScript/Interpreter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1005,7 +1005,7 @@ primitives = Map.fromList
, prim "write_coq_cryptol_primitives_for_sawcore" "String -> [(String, String)] -> [String] -> TopLevel ()"
(pureVal writeCoqCryptolPrimitivesForSAWCore)
Experimental
[ "Write out a representation of cryptol-verifier's Cryptol.sawcore in"
[ "Write out a representation of cryptol-saw-core's Cryptol.sawcore in"
, "Gallina syntax for Coq."
, "The first argument is the name of the file to output into,"
, "use an empty string to output to standard output."
Expand Down
2 changes: 1 addition & 1 deletion stack.ghc-8.6.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,12 @@ packages:
- deps/aig/
- deps/abcBridge/
- deps/cryptol/
- deps/saw-core/cryptol-saw-core/
- deps/saw-core/saw-core/
- deps/saw-core/saw-core-aig/
- deps/saw-core/saw-core-sbv/
- deps/saw-core/saw-core-what4/
- deps/saw-core-coq/
- deps/cryptol-verifier/
- deps/jvm-verifier/
- deps/what4/what4/
- deps/what4/what4-abc/
Expand Down
2 changes: 1 addition & 1 deletion stack.ghc-8.8.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,12 @@ packages:
- deps/aig/
- deps/abcBridge/
- deps/cryptol/
- deps/saw-core/cryptol-saw-core/
- deps/saw-core/saw-core/
- deps/saw-core/saw-core-aig/
- deps/saw-core/saw-core-sbv/
- deps/saw-core/saw-core-what4/
- deps/saw-core-coq/
- deps/cryptol-verifier/
- deps/jvm-verifier/
- deps/what4/what4/
- deps/what4/what4-abc/
Expand Down