mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-27 11:13:48 +03:00
Preparation for the 2.10 release (#972)
* Update CHANGES for 2.10 * Remove profiling flags from Cabal file They result in `cabal check` warnings and probably don’t need to be hard-coded. * Remove commented-out Cryptol server references The code no longer exists, so we’ll never uncomment these. Equivalent functionality is now provided by `cryptol-remote-api`. * Update references to version numbers in README. Closes #719.
This commit is contained in:
parent
5cbf17b425
commit
0541bcf559
58
CHANGES.md
58
CHANGES.md
@ -1,3 +1,61 @@
|
|||||||
|
# 2.10.0
|
||||||
|
|
||||||
|
## Language changes
|
||||||
|
|
||||||
|
* Cryptol now supports primality checking at the type level. The
|
||||||
|
type-level predicate `prime` is true when its parameter passes the
|
||||||
|
Miller-Rabin probabilistic primality test implemented in the GMP
|
||||||
|
library.
|
||||||
|
|
||||||
|
* The `Z p` type is now a `Field` when `p` is prime, allowing additional
|
||||||
|
operations on `Z p` values.
|
||||||
|
|
||||||
|
* The literals `0` and `1` can now be used at type `Bit`, as
|
||||||
|
alternatives for `False` and `True`, respectively.
|
||||||
|
|
||||||
|
## New features
|
||||||
|
|
||||||
|
* The interpreter now includes a number of primitive functions that
|
||||||
|
allow faster execution of a number of common cryptographic functions,
|
||||||
|
including the core operations of AES and SHA-2, operations on GF(2)
|
||||||
|
polynomials (the existing `pmod`, `pdiv`, and `pmult` functions), and
|
||||||
|
some operations on prime field elliptic curves. These functions are
|
||||||
|
useful for implementing higher-level algorithms, such as many
|
||||||
|
post-quantum schemes, with more acceptable performance than possible
|
||||||
|
when running a top-to-bottom Cryptol implementation in the
|
||||||
|
interpreter.
|
||||||
|
|
||||||
|
For a full list of the new primitives, see the new Cryptol
|
||||||
|
[`SuiteB`](https://github.com/GaloisInc/cryptol/blob/master/lib/SuiteB.cry)
|
||||||
|
and
|
||||||
|
[`PrimeEC`](https://github.com/GaloisInc/cryptol/blob/master/lib/PrimeEC.cry)
|
||||||
|
modules.
|
||||||
|
|
||||||
|
* The REPL now allows lines containing only comments, making it easier
|
||||||
|
to copy and paste examples.
|
||||||
|
|
||||||
|
* The interpreter has generally improved performance overall.
|
||||||
|
|
||||||
|
* Several error messages are more comprehensible and less verbose.
|
||||||
|
|
||||||
|
* Cryptol releases and nightly builds now include an RPC server
|
||||||
|
alongside the REPL. This provides an alternative interface to the same
|
||||||
|
interpreter and proof engine available from the REPL, but is
|
||||||
|
better-suited to programmatic use. Details on the protocol used by the
|
||||||
|
server are available
|
||||||
|
[here](https://github.com/GaloisInc/argo/blob/master/docs/Protocol.rst).
|
||||||
|
A Python client for this protocol is available
|
||||||
|
[here](https://github.com/GaloisInc/argo/tree/master/python).
|
||||||
|
|
||||||
|
* Windows builds are now distributed as both `.tar.gz` and `.msi` files.
|
||||||
|
|
||||||
|
## Bug Fixes
|
||||||
|
|
||||||
|
* Closed issues #98, #485, #713, #744, #746, #787, #796, #803, #818,
|
||||||
|
#826, #838, #856, #873, #875, #876, #877, #879, #880, #881, #883,
|
||||||
|
#886, #887, #888, #892, #894, #901, #910, #913, #924, #926, #931,
|
||||||
|
#933, #937, #939, #946, #948, #953, #956, #958, and #969.
|
||||||
|
|
||||||
# 2.9.1
|
# 2.9.1
|
||||||
|
|
||||||
## Language changes
|
## Language changes
|
||||||
|
@ -46,7 +46,9 @@ Cryptol currently uses Microsoft Research's [Z3 SMT
|
|||||||
solver](https://github.com/Z3Prover/z3) by default to solve constraints
|
solver](https://github.com/Z3Prover/z3) by default to solve constraints
|
||||||
during type checking, and as the default solver for the `:sat` and
|
during type checking, and as the default solver for the `:sat` and
|
||||||
`:prove` commands. Cryptol generally requires the most recent version
|
`:prove` commands. Cryptol generally requires the most recent version
|
||||||
of Z3, which at the time of writing this file is 4.8.8.
|
of Z3, but you can see the specific version tested in CI by looking for
|
||||||
|
the `Z3_VERSION` setting in [this
|
||||||
|
file](https://github.com/GaloisInc/cryptol/blob/master/.github/workflows/build.yml).
|
||||||
|
|
||||||
You can download Z3 binaries for a variety of platforms from their
|
You can download Z3 binaries for a variety of platforms from their
|
||||||
[releases page](https://github.com/Z3Prover/z3/releases). If you
|
[releases page](https://github.com/Z3Prover/z3/releases). If you
|
||||||
@ -81,8 +83,8 @@ Windows. We regularly build and test it in the following environments:
|
|||||||
## Prerequisites
|
## Prerequisites
|
||||||
|
|
||||||
Cryptol is regularly built and tested with the three most recent
|
Cryptol is regularly built and tested with the three most recent
|
||||||
versions of GHC, which at the time of this writing are 8.6.5, 8.8.3, and
|
versions of GHC, which at the time of this writing are 8.6.5, 8.8.4, and
|
||||||
8.10.1. The easiest way to install an approporiate version of GHC is
|
8.10.2. The easiest way to install an approporiate version of GHC is
|
||||||
with [ghcup](https://www.haskell.org/ghcup/).
|
with [ghcup](https://www.haskell.org/ghcup/).
|
||||||
|
|
||||||
Some supporting non-Haskell libraries are required to build
|
Some supporting non-Haskell libraries are required to build
|
||||||
|
@ -37,11 +37,6 @@ flag relocatable
|
|||||||
default: True
|
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.
|
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.
|
||||||
|
|
||||||
-- Note: the Cryptol server needs to be updated to some new APIs.
|
|
||||||
--flag server
|
|
||||||
-- default: False
|
|
||||||
-- description: Build with the ZeroMQ/JSON cryptol-server executable
|
|
||||||
|
|
||||||
library
|
library
|
||||||
Default-language:
|
Default-language:
|
||||||
Haskell2010
|
Haskell2010
|
||||||
@ -207,8 +202,6 @@ library
|
|||||||
if impl(ghc >= 8.0.1)
|
if impl(ghc >= 8.0.1)
|
||||||
ghc-options: -Wno-redundant-constraints
|
ghc-options: -Wno-redundant-constraints
|
||||||
|
|
||||||
ghc-prof-options: -O2 -fprof-auto-top
|
|
||||||
|
|
||||||
if flag(relocatable)
|
if flag(relocatable)
|
||||||
cpp-options: -DRELOCATABLE
|
cpp-options: -DRELOCATABLE
|
||||||
|
|
||||||
@ -239,8 +232,6 @@ executable cryptol
|
|||||||
if impl(ghc >= 8.0.1)
|
if impl(ghc >= 8.0.1)
|
||||||
ghc-options: -Wno-redundant-constraints
|
ghc-options: -Wno-redundant-constraints
|
||||||
|
|
||||||
ghc-prof-options: -O2 -fprof-auto-top
|
|
||||||
|
|
||||||
if os(linux) && flag(static)
|
if os(linux) && flag(static)
|
||||||
ld-options: -static -pthread
|
ld-options: -static -pthread
|
||||||
|
|
||||||
@ -252,37 +243,6 @@ executable cryptol-html
|
|||||||
build-depends: base, text, cryptol, blaze-html
|
build-depends: base, text, cryptol, blaze-html
|
||||||
GHC-options: -Wall
|
GHC-options: -Wall
|
||||||
|
|
||||||
-- Note: the Cryptol server needs to be updated to some new APIs.
|
|
||||||
--executable cryptol-server
|
|
||||||
-- main-is: Main.hs
|
|
||||||
-- hs-source-dirs: cryptol-server
|
|
||||||
-- other-modules: Cryptol.Aeson
|
|
||||||
-- default-language: Haskell2010
|
|
||||||
-- default-extensions: OverloadedStrings
|
|
||||||
-- GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m"
|
|
||||||
-- if impl(ghc >= 8.0.1)
|
|
||||||
-- ghc-options: -Wno-redundant-constraints
|
|
||||||
-- if os(linux) && flag(static)
|
|
||||||
-- ld-options: -static -pthread
|
|
||||||
-- if flag(server)
|
|
||||||
-- build-depends: aeson >= 0.10
|
|
||||||
-- , aeson-pretty >= 0.7
|
|
||||||
-- , base
|
|
||||||
-- , base-compat
|
|
||||||
-- , bytestring >= 0.10
|
|
||||||
-- , containers
|
|
||||||
-- , cryptol
|
|
||||||
-- , filepath
|
|
||||||
-- , monad-control
|
|
||||||
-- , optparse-applicative >= 0.12
|
|
||||||
-- , text
|
|
||||||
-- , transformers
|
|
||||||
-- , unix
|
|
||||||
-- , unordered-containers >= 0.2
|
|
||||||
-- , zeromq4-haskell >= 0.6
|
|
||||||
-- else
|
|
||||||
-- buildable: False
|
|
||||||
|
|
||||||
benchmark cryptol-bench
|
benchmark cryptol-bench
|
||||||
type: exitcode-stdio-1.0
|
type: exitcode-stdio-1.0
|
||||||
main-is: Main.hs
|
main-is: Main.hs
|
||||||
|
Loading…
Reference in New Issue
Block a user