2020-10-28 03:40:39 +03:00
Cabal-version: 2.4
2014-04-18 21:18:26 +04:00
Name: cryptol
2021-10-05 20:11:28 +03:00
Version: 2.12.0.99
2014-04-18 02:34:25 +04:00
Synopsis: Cryptol: The Language of Cryptography
2015-03-10 01:16:53 +03:00
Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
2020-10-28 03:40:39 +03:00
License: BSD-3-Clause
2015-06-26 23:45:26 +03:00
License-file: LICENSE
2014-04-18 02:34:25 +04:00
Author: Galois, Inc.
Maintainer: cryptol@galois.com
2015-03-10 01:16:53 +03:00
Homepage: http://www.cryptol.net/
Bug-reports: https://github.com/GaloisInc/cryptol/issues
2021-10-05 20:16:16 +03:00
Copyright: 2013-2021 Galois Inc.
2014-04-18 02:34:25 +04:00
Category: Language
2015-03-16 23:18:28 +03:00
Build-type: Simple
2016-05-20 22:04:53 +03:00
extra-source-files: bench/data/*.cry
2019-04-30 02:17:54 +03:00
CHANGES.md
2014-04-18 02:34:25 +04:00
2020-10-28 03:40:39 +03:00
data-files: **/*.cry **/*.z3
2015-01-22 02:03:16 +03:00
data-dir: lib
2014-04-18 02:34:25 +04:00
2015-03-10 01:16:53 +03:00
source-repository head
type: git
location: https://github.com/GaloisInc/cryptol.git
source-repository this
type: git
location: https://github.com/GaloisInc/cryptol.git
2020-11-10 20:36:05 +03:00
-- add a tag on release branches
-- tag:
2014-04-18 02:34:25 +04:00
flag static
default: False
description: Create a statically-linked binary
2015-03-04 03:22:14 +03:00
flag relocatable
default: True
description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution.
2014-04-18 02:34:25 +04:00
library
2014-09-15 01:37:37 +04:00
Default-language:
2017-10-24 21:59:34 +03:00
Haskell2010
2016-06-07 23:40:15 +03:00
Build-depends: base >= 4.8 && < 5,
2022-01-13 20:13:40 +03:00
arithmoi >= 0.12,
2020-06-30 20:09:49 +03:00
async >= 2.2 && < 2.3,
2020-03-01 09:12:39 +03:00
base-compat >= 0.6 && < 0.12,
2020-05-06 23:01:57 +03:00
bv-sized >= 1.0 && < 1.1,
2015-12-26 08:39:01 +03:00
bytestring >= 0.10,
2015-12-04 02:36:43 +03:00
array >= 0.4,
containers >= 0.5,
2019-02-28 01:37:39 +03:00
cryptohash-sha1 >= 0.11 && < 0.12,
2015-12-04 02:36:43 +03:00
deepseq >= 1.3,
2016-06-07 23:40:15 +03:00
directory >= 1.2.2.0,
2020-05-07 00:14:47 +03:00
exceptions,
2015-12-04 02:36:43 +03:00
filepath >= 1.3,
gitrev >= 1.0,
2020-09-24 22:50:37 +03:00
ghc-prim,
2015-12-04 02:36:43 +03:00
GraphSCC >= 1.0.4,
heredoc >= 0.2,
2021-01-29 02:24:15 +03:00
libBF >= 0.6 && < 0.7,
2020-05-19 01:42:17 +03:00
MemoTrie >= 0.6 && < 0.7,
2015-12-04 02:36:43 +03:00
monad-control >= 1.0,
monadLib >= 3.7.2,
2020-03-03 21:00:51 +03:00
parameterized-utils >= 2.0.2,
2021-08-07 00:10:33 +03:00
prettyprinter >= 1.7.0,
2022-05-25 02:25:32 +03:00
pretty-show,
2015-12-04 02:36:43 +03:00
process >= 1.2,
2022-01-12 17:33:24 +03:00
sbv >= 8.10 && < 8.17,
2021-06-30 01:22:04 +03:00
simple-smt >= 0.9.7,
2020-08-21 19:02:37 +03:00
stm >= 2.4,
2017-09-14 01:31:43 +03:00
strict,
2015-12-04 02:36:43 +03:00
text >= 1.1,
tf-random >= 0.5,
transformers-base >= 0.4,
2017-07-18 20:25:00 +03:00
mtl >= 2.2.1,
2020-03-03 21:00:51 +03:00
time >= 1.6.0.1,
panic >= 0.3,
2021-06-17 21:54:09 +03:00
what4 >= 1.2 && < 1.3
2017-09-27 00:02:52 +03:00
2022-01-13 20:13:40 +03:00
if impl(ghc >= 9.0)
build-depends: ghc-bignum >= 1.0 && < 1.3
else
build-depends: integer-gmp >= 1.0 && < 1.1
2020-11-10 20:36:05 +03:00
Build-tool-depends: alex:alex, happy:happy
2015-01-24 01:22:18 +03:00
hs-source-dirs: src
2014-04-18 02:34:25 +04:00
2020-03-09 21:29:08 +03:00
Exposed-modules: Cryptol.Parser,
2014-04-18 02:34:25 +04:00
Cryptol.Parser.Lexer,
2021-04-29 21:17:34 +03:00
Cryptol.Parser.Token,
Cryptol.Parser.Layout,
2014-04-18 02:34:25 +04:00
Cryptol.Parser.AST,
Cryptol.Parser.Position,
Cryptol.Parser.Names,
2015-09-25 00:47:52 +03:00
Cryptol.Parser.Name,
2014-04-18 02:34:25 +04:00
Cryptol.Parser.NoPat,
Cryptol.Parser.NoInclude,
2018-06-12 00:28:49 +03:00
Cryptol.Parser.Selector,
2014-04-18 02:34:25 +04:00
Cryptol.Parser.Utils,
Cryptol.Parser.Unlit,
2019-12-14 09:41:55 +03:00
Cryptol.Utils.Fixity,
2015-09-25 00:47:52 +03:00
Cryptol.Utils.Ident,
2020-06-27 02:37:54 +03:00
Cryptol.Utils.RecordMap,
2014-04-18 02:34:25 +04:00
Cryptol.Utils.PP,
Cryptol.Utils.Panic,
Cryptol.Utils.Debug,
2014-12-05 22:46:09 +03:00
Cryptol.Utils.Misc,
2017-02-09 02:08:50 +03:00
Cryptol.Utils.Patterns,
2017-10-05 01:50:31 +03:00
Cryptol.Utils.Logger,
2014-04-18 02:34:25 +04:00
Cryptol.Version,
Cryptol.ModuleSystem,
Cryptol.ModuleSystem.Base,
Cryptol.ModuleSystem.Env,
2019-02-28 01:37:39 +03:00
Cryptol.ModuleSystem.Fingerprint,
2014-04-18 02:34:25 +04:00
Cryptol.ModuleSystem.Interface,
Cryptol.ModuleSystem.Monad,
2015-05-21 23:42:54 +03:00
Cryptol.ModuleSystem.Name,
2021-12-22 16:05:46 +03:00
Cryptol.ModuleSystem.Names,
2014-04-18 02:34:25 +04:00
Cryptol.ModuleSystem.NamingEnv,
2021-12-22 16:05:46 +03:00
Cryptol.ModuleSystem.Binds
2017-10-03 01:01:45 +03:00
Cryptol.ModuleSystem.Exports,
Implementation of nested modules.
* Limitations:
Does not work in combination parameterized modules, as I am
about to redo how that works.
* General refeactorings:
* Namespaces:
- We have an explicit type for namespaces, see `Cryptol.Util.Ident`
- Display environments should now be aware of the namespace of the
name being displayed.
* Renamer:
- Factor out the renamer monad and error type into separate modules
- All name resultion is done through a single function `resolveName`
- The renamer now computes the dependencies between declarations,
orders things in dependency order, and checks for bad recursion.
* Typechecker: Redo checking of declarations (both top-level and local).
Previously we used a sort of CPS to add things in scope. Now we use
a state monad and add things to the state. We assume that the renamer
has been run, which means that declarations are ordered in dependency
order, and things have unique name, so we don't need to worry about
scoping too much.
* Change specific to nested modules:
- We have a new namespace for module names
- The interface file of a module contains the interfaces for nested modules
- Most of the changes related to nested modules in the renamer are
in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename`
- There is some trickiness when resolving module names when importing
submodules (seed `processOpen` and `openLoop`)
- There are some changes to the representation of modules in the typechecked
syntax, in particular:
- During type-checking we "flatten" nested module declarations into
a single big declaration. Hopefully, this means that passes after
the type checker don't need to worry about nested modules
- There is a new field containing the interfaces of the nested modules,
this is needed so that when we import the module we know we have the
nested structure
- Declarations in functor/parameterzied modules do not appear in the
flattened list of declarations. Instead thouse modules are collected
in a separate field, and the plan is that they would be used from
there when we implmenet functor instantiation.
2021-01-27 02:54:24 +03:00
Cryptol.ModuleSystem.Renamer,
2022-02-22 03:08:01 +03:00
Cryptol.ModuleSystem.Renamer.Imports,
2022-04-05 19:49:57 +03:00
Cryptol.ModuleSystem.Renamer.ImplicitImports,
Implementation of nested modules.
* Limitations:
Does not work in combination parameterized modules, as I am
about to redo how that works.
* General refeactorings:
* Namespaces:
- We have an explicit type for namespaces, see `Cryptol.Util.Ident`
- Display environments should now be aware of the namespace of the
name being displayed.
* Renamer:
- Factor out the renamer monad and error type into separate modules
- All name resultion is done through a single function `resolveName`
- The renamer now computes the dependencies between declarations,
orders things in dependency order, and checks for bad recursion.
* Typechecker: Redo checking of declarations (both top-level and local).
Previously we used a sort of CPS to add things in scope. Now we use
a state monad and add things to the state. We assume that the renamer
has been run, which means that declarations are ordered in dependency
order, and things have unique name, so we don't need to worry about
scoping too much.
* Change specific to nested modules:
- We have a new namespace for module names
- The interface file of a module contains the interfaces for nested modules
- Most of the changes related to nested modules in the renamer are
in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename`
- There is some trickiness when resolving module names when importing
submodules (seed `processOpen` and `openLoop`)
- There are some changes to the representation of modules in the typechecked
syntax, in particular:
- During type-checking we "flatten" nested module declarations into
a single big declaration. Hopefully, this means that passes after
the type checker don't need to worry about nested modules
- There is a new field containing the interfaces of the nested modules,
this is needed so that when we import the module we know we have the
nested structure
- Declarations in functor/parameterzied modules do not appear in the
flattened list of declarations. Instead thouse modules are collected
in a separate field, and the plan is that they would be used from
there when we implmenet functor instantiation.
2021-01-27 02:54:24 +03:00
Cryptol.ModuleSystem.Renamer.Monad,
Cryptol.ModuleSystem.Renamer.Error,
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck,
2017-01-31 05:14:10 +03:00
Cryptol.TypeCheck.Type,
2019-07-03 03:34:36 +03:00
Cryptol.TypeCheck.TCon,
2017-02-09 02:08:50 +03:00
Cryptol.TypeCheck.TypePat,
Cryptol.TypeCheck.SimpType,
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.AST,
2017-08-15 01:45:37 +03:00
Cryptol.TypeCheck.Parseable,
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.Monad,
Cryptol.TypeCheck.Infer,
Cryptol.TypeCheck.InferTypes,
Implementation of nested modules.
* Limitations:
Does not work in combination parameterized modules, as I am
about to redo how that works.
* General refeactorings:
* Namespaces:
- We have an explicit type for namespaces, see `Cryptol.Util.Ident`
- Display environments should now be aware of the namespace of the
name being displayed.
* Renamer:
- Factor out the renamer monad and error type into separate modules
- All name resultion is done through a single function `resolveName`
- The renamer now computes the dependencies between declarations,
orders things in dependency order, and checks for bad recursion.
* Typechecker: Redo checking of declarations (both top-level and local).
Previously we used a sort of CPS to add things in scope. Now we use
a state monad and add things to the state. We assume that the renamer
has been run, which means that declarations are ordered in dependency
order, and things have unique name, so we don't need to worry about
scoping too much.
* Change specific to nested modules:
- We have a new namespace for module names
- The interface file of a module contains the interfaces for nested modules
- Most of the changes related to nested modules in the renamer are
in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename`
- There is some trickiness when resolving module names when importing
submodules (seed `processOpen` and `openLoop`)
- There are some changes to the representation of modules in the typechecked
syntax, in particular:
- During type-checking we "flatten" nested module declarations into
a single big declaration. Hopefully, this means that passes after
the type checker don't need to worry about nested modules
- There is a new field containing the interfaces of the nested modules,
this is needed so that when we import the module we know we have the
nested structure
- Declarations in functor/parameterzied modules do not appear in the
flattened list of declarations. Instead thouse modules are collected
in a separate field, and the plan is that they would be used from
there when we implmenet functor instantiation.
2021-01-27 02:54:24 +03:00
Cryptol.TypeCheck.Interface,
2017-12-22 00:59:43 +03:00
Cryptol.TypeCheck.Error,
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.Kind,
Cryptol.TypeCheck.Subst,
Cryptol.TypeCheck.Instantiate,
Cryptol.TypeCheck.Unify,
Cryptol.TypeCheck.PP,
Cryptol.TypeCheck.Solve,
2017-12-23 03:01:19 +03:00
Cryptol.TypeCheck.Default,
2017-01-31 05:14:10 +03:00
Cryptol.TypeCheck.SimpleSolver,
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.TypeMap,
2014-05-10 03:27:07 +04:00
Cryptol.TypeCheck.TypeOf,
2015-05-20 00:25:56 +03:00
Cryptol.TypeCheck.Sanity,
2022-04-12 02:24:38 +03:00
Cryptol.TypeCheck.Module,
2022-06-01 02:50:38 +03:00
Cryptol.TypeCheck.ModuleInstance,
2014-04-18 02:34:25 +04:00
2017-02-01 01:12:53 +03:00
Cryptol.TypeCheck.Solver.Types,
2017-02-17 03:46:38 +03:00
Cryptol.TypeCheck.Solver.SMT,
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.Solver.InfNat,
Cryptol.TypeCheck.Solver.Class,
Cryptol.TypeCheck.Solver.Selector,
Cryptol.TypeCheck.Solver.Utils,
2017-01-31 05:14:10 +03:00
Cryptol.TypeCheck.Solver.Numeric,
2017-02-09 02:08:50 +03:00
Cryptol.TypeCheck.Solver.Improve,
2015-08-15 03:38:41 +03:00
Cryptol.TypeCheck.Solver.Numeric.Fin,
Cryptol.TypeCheck.Solver.Numeric.Interval,
2014-12-02 03:28:29 +03:00
2014-04-18 02:34:25 +04:00
Cryptol.Transform.MonoValues,
Cryptol.Transform.Specialize,
2017-10-28 00:59:32 +03:00
Cryptol.IR.FreeVars,
2021-12-30 19:05:17 +03:00
Cryptol.IR.TraverseNames,
2017-10-28 00:59:32 +03:00
2020-10-09 03:33:20 +03:00
Cryptol.Backend,
2020-10-09 03:43:19 +03:00
Cryptol.Backend.Arch,
2020-10-09 03:33:20 +03:00
Cryptol.Backend.Concrete,
Cryptol.Backend.FloatHelpers,
Cryptol.Backend.Monad,
2021-03-26 07:39:35 +03:00
Cryptol.Backend.SeqMap,
2020-10-09 03:33:20 +03:00
Cryptol.Backend.SBV,
Cryptol.Backend.What4,
2021-03-26 22:06:26 +03:00
Cryptol.Backend.WordValue,
2020-10-09 03:33:20 +03:00
2014-04-18 02:34:25 +04:00
Cryptol.Eval,
2020-03-09 21:29:08 +03:00
Cryptol.Eval.Concrete,
2014-04-18 02:34:25 +04:00
Cryptol.Eval.Env,
2020-03-10 00:09:19 +03:00
Cryptol.Eval.Generic,
2020-11-24 21:02:59 +03:00
Cryptol.Eval.Prims,
2017-02-03 20:02:25 +03:00
Cryptol.Eval.Reference,
2020-03-10 00:32:07 +03:00
Cryptol.Eval.SBV,
2014-04-18 02:34:25 +04:00
Cryptol.Eval.Type,
Cryptol.Eval.Value,
2020-03-03 21:00:51 +03:00
Cryptol.Eval.What4,
2014-04-18 02:34:25 +04:00
2020-09-15 04:35:29 +03:00
Cryptol.AES,
2020-10-01 21:37:21 +03:00
Cryptol.F2,
2020-09-04 19:03:58 +03:00
Cryptol.SHA,
2020-09-22 19:58:15 +03:00
Cryptol.PrimeEC,
2020-09-04 19:03:58 +03:00
2014-04-18 02:34:25 +04:00
Cryptol.Testing.Random,
2015-03-03 02:46:21 +03:00
Cryptol.Symbolic,
2020-03-24 02:57:31 +03:00
Cryptol.Symbolic.SBV,
2020-03-25 01:57:42 +03:00
Cryptol.Symbolic.What4,
2014-04-18 02:34:25 +04:00
2015-03-03 02:46:21 +03:00
Cryptol.REPL.Command,
2022-01-13 01:05:07 +03:00
Cryptol.REPL.Help,
2021-04-03 02:07:48 +03:00
Cryptol.REPL.Browse,
2015-03-03 02:46:21 +03:00
Cryptol.REPL.Monad,
Cryptol.REPL.Trie
2014-04-18 02:34:25 +04:00
2014-08-06 20:49:19 +04:00
Other-modules: Cryptol.Parser.LexerUtils,
Cryptol.Parser.ParserUtils,
2015-03-06 02:14:09 +03:00
Cryptol.Prelude,
2022-01-13 20:13:40 +03:00
GHC.Num.Compat,
2014-04-18 21:28:46 +04:00
Paths_cryptol,
2014-04-18 02:34:25 +04:00
GitRev
2020-03-30 23:01:06 +03:00
GHC-options: -Wall -fsimpl-tick-factor=140 -O2
2016-06-28 00:56:55 +03:00
if impl(ghc >= 8.0.1)
ghc-options: -Wno-redundant-constraints
2014-04-18 02:34:25 +04:00
2015-03-04 03:22:14 +03:00
if flag(relocatable)
cpp-options: -DRELOCATABLE
2014-04-18 02:34:25 +04:00
executable cryptol
2014-09-15 01:37:37 +04:00
Default-language:
2017-10-24 21:59:34 +03:00
Haskell2010
2014-04-18 02:34:25 +04:00
Main-is: Main.hs
hs-source-dirs: cryptol
2020-11-10 20:36:05 +03:00
Autogen-modules: Paths_cryptol
2014-04-18 02:34:25 +04:00
Other-modules: OptParser,
REPL.Haskeline,
2015-01-28 22:28:52 +03:00
REPL.Logo,
2014-04-18 21:28:46 +04:00
Paths_cryptol
2020-11-10 20:36:05 +03:00
2015-02-06 04:05:11 +03:00
build-depends: ansi-terminal
, base
2015-10-09 02:54:08 +03:00
, base-compat
2018-07-31 04:11:08 +03:00
, containers
2015-02-06 04:05:11 +03:00
, cryptol
, directory
, filepath
2020-05-07 00:14:47 +03:00
, haskeline >= 0.7 && < 0.9
2021-06-30 01:22:04 +03:00
, exceptions
2015-12-04 02:36:43 +03:00
, monad-control
2017-10-05 05:15:42 +03:00
, text
2015-02-06 04:05:11 +03:00
, transformers
2020-03-30 23:01:06 +03:00
GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2
2016-06-28 00:56:55 +03:00
if impl(ghc >= 8.0.1)
ghc-options: -Wno-redundant-constraints
2014-04-18 02:34:25 +04:00
if os(linux) && flag(static)
2021-03-24 01:24:48 +03:00
ld-options: -static -pthread
ghc-options: -optl-fuse-ld=bfd
2015-07-08 04:13:34 +03:00
2017-10-25 21:12:37 +03:00
executable cryptol-html
2018-08-01 18:59:54 +03:00
Default-language:
Haskell2010
2017-10-25 21:12:37 +03:00
main-is: CryHtml.hs
hs-source-dirs: utils
2018-03-06 04:07:19 +03:00
build-depends: base, text, cryptol, blaze-html
2017-10-25 21:12:37 +03:00
GHC-options: -Wall
2021-03-24 01:24:48 +03:00
if os(linux) && flag(static)
ld-options: -static -pthread
ghc-options: -optl-fuse-ld=bfd
2020-11-21 03:53:36 +03:00
executable check-exercises
Default-language:
Haskell2010
Main-is: CheckExercises.hs
hs-source-dirs: cryptol
build-depends: ansi-terminal
, base
, containers
, directory
, extra
, filepath
, mtl
, optparse-applicative
, process
, temporary
, text
GHC-options: -Wall
2015-08-10 21:24:36 +03:00
benchmark cryptol-bench
type: exitcode-stdio-1.0
main-is: Main.hs
hs-source-dirs: bench
default-language: Haskell2010
2020-03-30 23:01:06 +03:00
GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2
2016-06-28 00:56:55 +03:00
if impl(ghc >= 8.0.1)
ghc-options: -Wno-redundant-constraints
2015-08-10 21:24:36 +03:00
if os(linux) && flag(static)
2021-03-24 01:24:48 +03:00
ld-options: -static -pthread
ghc-options: -optl-fuse-ld=bfd
2015-08-10 21:24:36 +03:00
build-depends: base
, criterion
, cryptol
2015-08-10 23:52:01 +03:00
, deepseq
2017-03-21 22:31:04 +03:00
, directory
, filepath
2020-06-30 20:15:32 +03:00
, sbv
2015-08-10 21:24:36 +03:00
, text