GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Merge remote-tracking branch 'origin/master' into gitpod

Browse Source
This commit is contained in:
Lisanna Dettwyler 2021-06-12 11:48:06 +00:00
commit 6247bbfd59
34 changed files with 1949 additions and 708 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
.github/ci.sh vendored
View File

@ -1,5 +1,5 @@
#!/usr/bin/env bash
set -Eeuo pipefail
set -xEeuo pipefail
[[ "$RUNNER_OS" == 'Windows' ]] && IS_WIN=true || IS_WIN=false
BIN=bin
@ -37,13 +37,7 @@ retry() {
done
}
setup_external_tools() {
is_exe "$BIN" "test-runner" && return
cabal v2-install --install-method=copy --installdir="$BIN" test-lib
}
setup_dist_bins() {
is_exe "dist/bin" "cryptol" && is_exe "dist/bin" "cryptol-html" && return
extract_exe "cryptol" "dist/bin"
extract_exe "cryptol-html" "dist/bin"
extract_exe "cryptol-remote-api" "dist/bin"
@ -55,21 +49,19 @@ install_z3() {
is_exe "$BIN" "z3" && return
case "$RUNNER_OS" in
Linux) file="ubuntu-16.04" ;;
macOS) file="osx-10.14.6" ;;
Windows) file="win" ;;
Linux) file="ubuntu-18.04.zip" ;;
macOS) file="osx-10.15.7.zip" ;;
Windows) file="win.zip" ;;
esac
curl -o z3.zip -sL "https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/z3-$Z3_VERSION-x64-$file.zip"
curl -o z3.zip -sL "https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/z3-$Z3_VERSION-x64-$file"
if $IS_WIN; then 7z x -bd z3.zip; else unzip z3.zip; fi
cp z3-$Z3_VERSION-x64-$file/bin/z3$EXT $BIN/z3$EXT
rm -rf z3-$Z3_VERSION-x64-$file
cp z3-*/bin/z3$EXT $BIN/z3$EXT
$IS_WIN || chmod +x $BIN/z3
rm z3.zip
}
install_cvc4() {
is_exe "$BIN" "cvc4" && return
version="${CVC4_VERSION#4.}" # 4.y.z -> y.z
case "$RUNNER_OS" in
@ -89,7 +81,6 @@ install_cvc4() {
}
install_yices() {
is_exe "$BIN" "yices" && return
ext=".tar.gz"
case "$RUNNER_OS" in
Linux) file="pc-linux-gnu-static-gmp.tar.gz" ;;
@ -131,13 +122,6 @@ install_system_deps() {
is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
}
test_dist() {
setup_dist_bins
setup_external_tools
echo "test-runner version: $($BIN/test-runner --version)"
$BIN/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol tests
}
check_docs() {
./cry build exe:check-exercises
find ./docs/ProgrammingCryptol -name '*.tex' -print0 | xargs -0 -n1 cabal v2-exec check-exercises
@ -147,6 +131,10 @@ test_rpc() {
./cry rpc-test
}
check_rpc_docs() {
./cry rpc-docs
}
bundle_files() {
doc=dist/share/doc/cryptol
lib=dist/share/cryptol
@ -172,7 +160,7 @@ sign() {
zip_dist() {
: "${VERSION?VERSION is required as an environment variable}"
name="${name:-"cryptol-$VERSION-$RUNNER_OS-x86_64"}"
mv dist "$name"
cp -r dist "$name"
tar -cvzf "$name".tar.gz "$name"
}

299
.github/workflows/ci.yml vendored
View File

@ -1,20 +1,15 @@
name: Cryptol
on:
push:
tags: ["v?[0-9]+.[0-9]+(.[0-9]+)?"]
tags: ["?[0-9]+.[0-9]+(.[0-9]+)?"]
branches: [master, "release-**"]
pull_request:
schedule:
- cron: "0 0 * * *"
- cron: "0 10 * * *" # 10am UTC -> 2/3am PST
workflow_dispatch:
inputs:
publish:
description: "Publish release artifacts"
required: false
default: "false"
env:
Z3_VERSION: "4.8.8"
Z3_VERSION: "4.8.10"
CVC4_VERSION: "4.1.8"
YICES_VERSION: "2.6.2"
@ -22,50 +17,35 @@ jobs:
config:
runs-on: ubuntu-latest
outputs:
changed: ${{ steps.getconf.outputs.changed-files }}
cryptol-version: ${{ steps.getconf.outputs.cryptol-version }}
name: ${{ steps.getconf.outputs.name }}
publish: ${{ steps.getconf-publish.outputs.publish }}
release: ${{ steps.getconf-release.outputs.release }}
retention-days: ${{ steps.getconf-retention.outputs.retention-days }}
name: ${{ steps.config.outputs.name }}
version: ${{ steps.config.outputs.version }}
event-tag: ${{ steps.config.outputs.tag }}
event-schedule: ${{ steps.config.outputs.schedule }}
release: ${{ steps.config.outputs.release }}
retention-days: ${{ steps.config.outputs.retention-days }}
steps:
- uses: actions/checkout@v2
with:
fetch-depth: 0
- name: getconf
id: getconf
run: |
set -x
.github/ci.sh set_files ${{ github.sha }}
.github/ci.sh set_version
.github/ci.sh output name cryptol-$(.github/ci.sh ver)
- name: getconf-publish
id: getconf-publish
if: |
(github.event_name == 'push' && startsWith(github.event.ref, 'refs/tags/')) ||
(github.event_name == 'schedule') ||
(github.event_name == 'workflow_dispatch' && github.event.inputs.publish == 'true')
run: |
set -x
.github/ci.sh output publish true
- name: getconf-release
id: getconf-release
if: startsWith(github.event.ref, 'refs/heads/release-')
run: |
set -x
.github/ci.sh output release true
- name: getconf-retention
id: getconf-retention
- name: config
id: config
env:
RELEASE: ${{ steps.getconf-release.outputs.release }}
shell: bash
EVENT_TAG: ${{ startsWith(github.event.ref, 'refs/tags/') }}
EVENT_SCHEDULE: ${{ github.event_name == 'schedule' }}
EVENT_DISPATCH: ${{ github.event_name == 'workflow_dispatch' }}
run: |
set -x
if [[ "$RELEASE" == "true" ]]; then
.github/ci.sh output retention-days 90
else
.github/ci.sh output retention-days 5
fi
.github/ci.sh output name cryptol-$(.github/ci.sh ver)
.github/ci.sh output version $(.github/ci.sh ver)
.github/ci.sh output tag $EVENT_TAG
.github/ci.sh output schedule $EVENT_SCHEDULE
RELEASE=$( \
[[ "refs/heads/release-$(.github/ci.sh ver)" == "${{ github.event.ref }}" ]] && \
[[ "refs/heads/release-$(git describe --tags --abbrev=0)" == "${{ github.event.ref }}" ]] && \
echo true || echo false)
.github/ci.sh output release $RELEASE
.github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5)
build:
runs-on: ${{ matrix.os }}
@ -74,11 +54,16 @@ jobs:
fail-fast: false
matrix:
os: [ubuntu-latest, macos-latest, windows-latest]
ghc: ["8.6.5", "8.8.4", "8.10.2"]
ghc-version: ["8.6.5", "8.8.4", "8.10.2"]
exclude:
# https://gitlab.haskell.org/ghc/ghc/-/issues/18550
- os: windows-latest
ghc: 8.10.2
ghc-version: 8.10.2
outputs:
test-lib-json: ${{ steps.test-lib.outputs.targets-json }}
env:
VERSION: ${{ needs.config.outputs.version }}
RELEASE: ${{ needs.config.outputs.release }}
steps:
- uses: actions/checkout@v2
with:
@ -92,10 +77,10 @@ jobs:
with:
poetry-version: 1.1.6
- uses: actions/setup-haskell@v1
- uses: haskell/actions/setup@v1
id: setup-haskell
with:
ghc-version: ${{ matrix.ghc }}
ghc-version: ${{ matrix.ghc-version }}
- uses: actions/cache@v2
name: Cache cabal store
@ -103,46 +88,30 @@ jobs:
path: |
${{ steps.setup-haskell.outputs.cabal-store }}
dist-newstyle
key: cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }}
key: cabal-${{ runner.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}-${{ github.sha }}
restore-keys: |
cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-
cabal-${{ runner.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}-
- shell: bash
run: .github/ci.sh install_system_deps
- shell: bash
run: .github/ci.sh setup_external_tools
- shell: bash
env:
RELEASE: ${{ needs.config.outputs.release }}
run: .github/ci.sh build
- shell: bash
run: .github/ci.sh setup_dist_bins
- shell: bash
run: .github/ci.sh check_docs
if: runner.os != 'Windows'
- shell: bash
run: .github/ci.sh test_dist
# TODO: get Python client to work on Windows
- shell: bash
run: .github/ci.sh test_rpc
run: .github/ci.sh check_rpc_docs
if: runner.os != 'Windows'
- if: matrix.ghc == '8.8.4'
uses: actions/upload-artifact@v2
with:
path: dist/bin
name: ${{ runner.os }}-bins
retention-days: ${{ needs.config.outputs.retention-days }}
build-docs:
runs-on: ubuntu-latest
needs: [config]
steps:
- uses: actions/checkout@v2
- uses: docker://pandoc/latex:2.9.2
- if: runner.os == 'Linux'
uses: docker://pandoc/latex:2.9.2
with:
args: >-
sh -c
@ -152,34 +121,20 @@ jobs:
cd docs &&
make
"
- uses: actions/upload-artifact@v2
with:
path: docs
name: docs
retention-days: ${{ needs.config.outputs.retention-days }}
bundle:
runs-on: ${{ matrix.os }}
strategy:
fail-fast: false
matrix:
os: [ubuntu-latest, macos-latest, windows-latest]
needs: [config, build-docs, build]
env:
VERSION: ${{ needs.config.outputs.cryptol-version }}
RELEASE: ${{ needs.config.outputs.release }}
steps:
- uses: actions/checkout@v2
- uses: actions/download-artifact@v2
with:
path: dist/bin
name: ${{ runner.os }}-bins
- uses: actions/download-artifact@v2
with:
path: docs
name: docs
- shell: bash
name: Partition test-lib tests
id: test-lib
run: |
set -x
cabal v2-install --install-method=copy --installdir="./bin" test-lib
cmd="cat \$1.stdout"
if ${{ runner.os == 'Windows' }}; then
cmd="cat \$1.stdout.mingw32 2>/dev/null || $cmd"
fi
./bin/test-runner --ext=.icry -r ./output --exe=$(which bash) -F -c -F "$cmd" -F -- ./tests
TARGETS_JSON=$(echo -n "$(ls -1 ./output/tests)" | jq -Rsc 'split("\n")')
echo "::set-output name=targets-json::$TARGETS_JSON"
- shell: bash
run: .github/ci.sh bundle_files
@ -194,11 +149,6 @@ jobs:
SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
run: .github/ci.sh sign cryptol.msi
- shell: bash
run: |
echo "NAME=${{ needs.config.outputs.name }}-${{ runner.os }}-x86_64" >> $GITHUB_ENV
.github/ci.sh zip_dist $NAME
- if: needs.config.outputs.release == 'true'
shell: bash
env:
@ -206,6 +156,12 @@ jobs:
SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
run: .github/ci.sh sign ${NAME}.tar.gz
- shell: bash
run: |
NAME="${{ needs.config.outputs.name }}-${{ runner.os }}-x86_64"
echo "NAME=$NAME" >> $GITHUB_ENV
.github/ci.sh zip_dist $NAME
- uses: actions/upload-artifact@v2
with:
name: ${{ env.NAME }}
@ -213,6 +169,18 @@ jobs:
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}
- if: matrix.ghc-version == '8.6.5'
uses: actions/upload-artifact@v2
with:
path: dist/bin
name: ${{ runner.os }}-dist-bin
- if: matrix.ghc-version == '8.6.5'
uses: actions/upload-artifact@v2
with:
path: bin
name: ${{ runner.os }}-bin
- uses: actions/upload-artifact@v2
if: runner.os == 'Windows'
with:
@ -221,6 +189,85 @@ jobs:
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}
test:
runs-on: ${{ matrix.os }}
needs: [build]
strategy:
fail-fast: false
matrix:
suite: [test-lib]
target: ${{ fromJson(needs.build.outputs.test-lib-json) }}
os: [ubuntu-latest, macos-latest, windows-latest]
continue-on-error: [false]
include:
- suite: rpc
target: ''
os: ubuntu-latest
continue-on-error: false
- suite: rpc
target: ''
os: macos-latest
continue-on-error: false
- suite: rpc
target: ''
os: windows
continue-on-error: true # TODO: get Python client to work on Windows
steps:
- uses: actions/checkout@v2
with:
submodules: true
- uses: haskell/actions/setup@v1
with:
ghc-version: '8.10.2'
- if: matrix.suite == 'rpc'
uses: actions/setup-python@v2
with:
python-version: '3.7'
- if: matrix.suite == 'rpc'
uses: abatilo/actions-poetry@v2.1.2
with:
poetry-version: 1.1.6
- uses: actions/download-artifact@v2
with:
name: "${{ runner.os }}-dist-bin"
path: dist/bin
- uses: actions/download-artifact@v2
with:
name: "${{ runner.os }}-bin"
path: bin
- shell: bash
run: |
set -x
chmod +x dist/bin/cryptol
chmod +x dist/bin/cryptol-remote-api
chmod +x dist/bin/cryptol-eval-server
chmod +x bin/test-runner
.github/ci.sh install_system_deps
ghc_ver="$(ghc --numeric-version)"
cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
cabal v2-update
- if: matrix.suite == 'test-lib'
shell: bash
continue-on-error: ${{ matrix.continue-on-error }}
name: test-lib ${{ matrix.target }}
run: |
export PATH=$PWD/bin:$PWD/dist/bin:$PATH
./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }}
- if: matrix.suite == 'rpc'
shell: bash
continue-on-error: ${{ matrix.continue-on-error }}
run: |
export PATH=$PWD/bin:$PWD/dist/bin:$PATH
cryptol-remote-api/run_rpc_tests.sh
build-push-image:
runs-on: ubuntu-latest
needs: [config]
@ -258,18 +305,6 @@ jobs:
with:
images: ${{ matrix.image }}
- if: needs.config.outputs.publish == 'true'
uses: crazy-max/ghaction-docker-meta@v1
name: Tags
id: tags
with:
images: ${{ matrix.image }}
tag-semver: |
${{ steps.prefix.outputs.prefix }}{{version}}
${{ steps.prefix.outputs.prefix }}{{major}}.{{minor}}
tag-schedule: |
${{ steps.prefix.outputs.prefix }}nightly
- uses: docker/login-action@v1
with:
registry: ghcr.io
@ -278,25 +313,26 @@ jobs:
- uses: docker/build-push-action@v2
with:
tags: |
${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
${{ steps.tags.outputs.tags }}
tags: ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
labels: ${{ steps.labels.outputs.labels }}
load: true
push: false
file: ${{ matrix.file }}
build-args: ${{ matrix.build-args }}
cache-from: |
type=registry,ref=${{ matrix.cache }}:${{ steps.prefix.outputs.prefix }}master
type=registry,ref=${{ matrix.cache }}:${{ steps.common-tag.outputs.common-tag }}
type=registry,ref=${{ matrix.cache }}:cache-${{ steps.prefix.outputs.prefix }}master
type=registry,ref=${{ matrix.cache }}:cache-${{ steps.common-tag.outputs.common-tag }}
- name: Cache image build
uses: docker/build-push-action@v2
continue-on-error: true # Tolerate cache upload failures - this should be handled better
with:
tags: ${{ matrix.cache }}:${{ steps.common-tag.outputs.common-tag }}
labels: ${{ steps.labels.outputs.labels }}
push: true
file: ${{ matrix.file }}
build-args: ${{ matrix.build-args }}
cache-to: type=registry,ref=${{ matrix.cache }}:${{ steps.common-tag.outputs.common-tag }},mode=max
cache-to: type=registry,ref=${{ matrix.cache }}:cache-${{ steps.common-tag.outputs.common-tag }},mode=max
- if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
uses: actions/checkout@v2
@ -307,7 +343,7 @@ jobs:
python-version: '3.7'
- if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
uses: abatilo/actions-poetry@v2.0.0
uses: abatilo/actions-poetry@v2.1.2
with:
poetry-version: 1.1.6
@ -352,5 +388,16 @@ jobs:
--restart=Never \
-- socket cra-socket-cryptol-remote-api 8080
- if: needs.config.outputs.publish == 'true'
run: docker push --all-tags ${{ matrix.image }}
- if: needs.config.outputs.event-schedule == 'true'
name: ${{ matrix.image }}:nightly
run: |
docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:nightly
docker push ${{ matrix.image }}:nightly
- if: needs.config.outputs.release == 'true'
name: ${{ matrix.image }}:${{ needs.config.outputs.version }}
run: |
docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }}
docker push ${{ matrix.image }}:${{ needs.config.outputs.version }}
docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest
docker push ${{ matrix.image }}:latest

7
cry
View File

@ -21,6 +21,7 @@ Available commands:
test Run some tests (may take a while)
quick-test Like "test" but run fewer tests by default
rpc-test Run RPC server tests
rpc-docs Check that the RPC documentation is up-to-date
exe-path Print the location of the local executable
EOM
}
@ -90,6 +91,12 @@ case $COMMAND in
$DIR/cryptol-remote-api/run_rpc_tests.sh
;;
rpc-docs)
echo "Checking cryptol-remote-api docs (Cryptol.rst) are up-to-date with server"
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
$DIR/cryptol-remote-api/check_docs.sh
;;
help) show_usage && exit 0 ;;

14
cryptol-remote-api/check_docs.sh Executable file
View File

@ -0,0 +1,14 @@
#! /bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
cd $DIR/docs
export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api)
if [[ ! -x "$CRYPTOL_SERVER" ]]; then
echo "could not locate cryptol-remote-api executable - try executing with cabal v2-exec"
exit 1
fi
$CRYPTOL_SERVER doc > TEMP.rst
diff Cryptol.rst TEMP.rst

8
cryptol-remote-api/cryptol-eval-server/Main.hs
View File

@ -36,6 +36,8 @@ import qualified Argo.Doc as Doc
import CryptolServer
( ServerState, moduleEnv, tcSolver, initialState, extendSearchPath, command, notification )
import CryptolServer.Call ( call )
import CryptolServer.Data.Expression ( Expression )
import CryptolServer.Data.Type ( JSONSchema )
import CryptolServer.EvalExpr
( evalExpressionDescr, evalExpression )
import CryptolServer.ExtendSearchPath
@ -90,7 +92,11 @@ evalServerDocs =
[ Doc.Section "Summary" $ [ Doc.Paragraph
[Doc.Text "A remote server for ",
Doc.Link (Doc.URL "https://https://cryptol.net/") "Cryptol",
Doc.Text " that supports only type checking and evaluation of Cryptol code."]]]
Doc.Text " that supports only type checking and evaluation of Cryptol code."]]
, Doc.Section "Terms and Types"
[Doc.datatype @Expression,
Doc.datatype @JSONSchema]
]
description :: String
description =

8
cryptol-remote-api/cryptol-remote-api/Main.hs
View File

@ -18,6 +18,8 @@ import CryptolServer.Call ( call, callDescr )
import CryptolServer.Check ( check, checkDescr )
import CryptolServer.ClearState
( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr )
import CryptolServer.Data.Expression ( Expression )
import CryptolServer.Data.Type ( JSONSchema )
import CryptolServer.EvalExpr
( evalExpression, evalExpressionDescr )
import CryptolServer.ExtendSearchPath
@ -47,7 +49,11 @@ serverDocs =
[ Doc.Section "Summary" $ [ Doc.Paragraph
[Doc.Text "An RCP server for ",
Doc.Link (Doc.URL "https://https://cryptol.net/") "Cryptol",
Doc.Text " that supports type checking and evaluation of Cryptol code via the methods documented below."]]]
Doc.Text " that supports type checking and evaluation of Cryptol code via the methods documented below."]]
, Doc.Section "Terms and Types"
[Doc.datatype @Expression,
Doc.datatype @JSONSchema]
]
description :: String
description =

1
cryptol-remote-api/docs/.gitignore vendored
View File

@ -1 +1,2 @@
_build/
TEMP.rst

775
cryptol-remote-api/docs/Cryptol.rst
View File

@ -1,353 +1,608 @@
==================
Cryptol Evaluation
Cryptol RPC Server
==================
All methods in this section additionally propagate server state in the
manner described in the prior section.
These methods may return :ref:`a variety of Cryptol errors
<cryptol-server-errors>`, with codes in the range of ``20000``-``29999``.
Options
=======
Many of the options that can be set using the ``:set`` command at the
Cryptol REPL can be provided as parameters to methods in this API. In
addition to the listed fields, every command accepts an optional
``options`` parameter. Its value should be an object, and may have
zero or more of the following fields:
- ``call stacks``: A Boolean that determines whether to track call stacks.
- ``output``: An object that contains further parameters to control strings generated by Cryptol (these are visible in e.g. error messages, but do not affect the structured data returned in the API):
+ ``ASCII``: A Boolean (default ``true``).
+ ``base``: What base to display numbers in (default ``10``).
+ ``prefix of infinite lengths``: How much of an infinite sequence to display (default ``5``.
+ ``floating point base``: What base to display floating point numbers in (default ``10``).
+ ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fpFormat`` in the REPL).
Module Management
=================
Changing Directories
Fundamental Protocol
--------------------
:Method name:
``change directory``
:Parameters:
- ``directory``: The new working directory, represented as a string.
This application is a `JSON-RPC <https://www.jsonrpc.org/specification>`_ server. Additionally, it maintains a persistent cache of application states and explicitly indicates the state in which each command is to be carried out.
Loading Modules
---------------
Transport
~~~~~~~~~
:Method name:
``load module``
:Parameters:
- ``module name``: The name of the Cryptol module to be loaded.
The server supports three transport methods:
Loading Files
-------------
:Method name:
``load file``
:Parameters:
- ``file``: The name of the Cryptol source file to be loaded.
``stdio``
in which the server communicates over ``stdin`` and ``stdout``
Module Context
--------------
Socket
in which the server communicates over ``stdin`` and ``stdout``
:Method name:
``focused module``
:Parameters: none
:Return fields:
- ``module``: The name of the focused module, which would be shown in the
prompt in the Cryptol REPL, or ``null`` if there is no such focused module.
- ``parameterized``: A Boolean value indicating whether the focused module is
parameterized. This field is only present when the module name is not
``null``.
HTTP
in which the server communicates over HTTP
In both ``stdio`` and socket mode, messages are delimited using `netstrings. <http://cr.yp.to/proto/netstrings.txt>`_
Evaluation and Typechecking
===========================
Evaluating Expressions
----------------------
Application State
~~~~~~~~~~~~~~~~~
This method evaluates a Cryptol expression. The type of the expression
needs to be fully-determined and finite - that is, functions and
infinite streams are not supported, and neither is polymorphism.
According to the JSON-RPC specification, the ``params`` field in a message object must be an array or object. In this protocol, it is always an object. While each message may specify its own arguments, every message has a parameter field named ``state``.
:Method name:
``evaluate expression``
:Parameters:
- ``expression``: The :ref:`JSON Cryptol expression <cryptol-json-expression>` to be evaluated
:Return fields:
- ``value``: A :ref:`JSON Cryptol expression <cryptol-json-expression>` that denotes the value
- ``type``: A :ref:`JSON Cryptol type <cryptol-json-type>` that denotes the result type
- ``type string``: A human-readable representation of the result type
When the first message is sent from the client to the server, the ``state`` parameter should be initialized to the JSON null value ``null``. Replies from the server may contain a new state that should be used in subsequent requests, so that state changes executed by the request are visible. Prior versions of this protocol represented the initial state as the empty array ``[]``, but this is now deprecated and will be removed.
Calling Functions
-----------------
In particular, per JSON-RPC, non-error replies are always a JSON object that contains a ``result`` field. The result field always contains an ``answer`` field and a ``state`` field, as well as ``stdout`` and ``stderr``.
Note: this method may be removed in the future, because its abilities
have been subsumed by ``evaluate expression``.
This method applies a Cryptol function to some arguments. The type of
the resulting expression needs to be fully-determined and finite -
that is, functions and infinite streams are not supported, and neither
is polymorphism.
``answer``
The value returned as a response to the request (the precise contents depend on which request was sent)
:Method name:
``call``
:Parameters:
- ``function``: The name of a Cryptol function that is currently in scope
- ``arguments``: A list of arguments to the function, encoded as JSON
Cryptol expressions
:Return fields:
- ``value``: A :ref:`JSON Cryptol expression <cryptol-json-expression>` that denotes the value
- ``type``: A :ref:`JSON Cryptol type <cryptol-json-type>` that denotes the result type
- ``type string``: A human-readable representation of the result type
``state``
The state, to be sent in subsequent requests. If the server did not modify its state in response to the command, then this state may be the same as the one sent by the client.
Visible Names
-------------
``stdout`` and ``stderr``
These fields contain the contents of the Unix ``stdout`` and ``stderr`` file descriptors. They are intended as a stopgap measure for clients who are still in the process of obtaining structured information from the libraries on which they depend, so that information is not completely lost to users. However, the server may or may not cache this information and resend it. Applications are encouraged to used structured data and send it deliberately as the answer.
The precise structure of states is considered an implementation detail that could change at any time. Please treat them as opaque tokens that may be saved and re-used within a given server process, but not created by the client directly.
Return information about all names in scope.
:Method name:
``visible names``
:Parameters: none
:Return value:
A list of name information objects. Each name information object has the following
fields:
- ``name``: A human-readable representation of the name
- ``type string``: A human-readable representation of the name's type schema
- ``type``: A :ref:`JSON Cryptol type <cryptol-json-type>`
Summary
-------
Some will additionally have the following field:
An RCP server for `Cryptol <https://https://cryptol.net/>`_ that supports type checking and evaluation of Cryptol code via the methods documented below.
- ``documentation``: The documentation string for the name, if it is documented
Checking Types
--------------
Check the type of an expression.
:Method name:
``check type``
:Parameters:
- ``expression``: A :ref:`JSON Cryptol expression <cryptol-json-expression>` for which a type is desired.
:Return fields:
- ``type schema``: A :ref:`JSON Cryptol type <cryptol-json-type>`
SAT
---
This method is not yet ready for public consumption.
Terms and Types
===============
.. _cryptol-json-expression:
---------------
.. _Expression:
JSON Cryptol Expressions
------------------------
~~~~~~~~~~~~~~~~~~~~~~~~
In the API, Cryptol expressions can be represented by the following:
JSON Booleans
Represent the corresponding Cryptol Booleans
JSON Integers
Cryptol integer literals, that can be used at a variety of types
JSON Strings
Cryptol concrete syntax
JSON Objects
Objects can represent a variety of Cryptol expressions. The field
``expression`` contains a tag that can be used to determine the
remaining fields.
Objects can represent a variety of Cryptol expressions. The field ``expression`` contains a tag that can be used to determine the remaining fields.
The tag values in objects can be:
``bits``
The expression is a bitvector. Further fields are:
+ ``encoding``: Either the string ``base64`` or ``hex``, for base-64 or hexadecimal
representations of the bitvector
+ ``data``: A string containing the actual data
+ ``width``: An integer: the bit-width of the represented bit vector
``bits``
* The expression is a bitvector. Further fields are:
* ``encoding``: Either the string ``base64`` or ``hex``, for base-64 or hexadecimal representations of the bitvector
* ``data``: A string containing the actual data
* ``width``: An integer: the bit-width of the represented bit vector
``record``
The expression is a record. The field ``data`` is a JSON
object that maps record field names to :ref:`JSON Cryptol expressions <cryptol-json-expression>`.
The expression is a record. The field ``data`` is a JSON object that maps record field names to :ref:`JSON Cryptol expressions <Expression>`.
``sequence``
The expression is a sequence. The field ``data`` contains a
JSON array of the elements of the sequence; each is a JSON Cryptol
expression.
The expression is a sequence. The field ``data``contains a JSON array of the elements of the sequence; each is a JSON Cryptol expression.
``tuple``
The expression is a tuple. The field ``data`` contains a JSON
array of the elements of the tuple; each is a JSON Cryptol
expression.
The expression is a tuple. The field ``data``contains a JSON array of the elements of the tuple; each is a JSON Cryptol expression.
``unit``
The expression is the unit constructor, and there are no further fields.
``let``
The expression is a ``where`` binding. The fields are:
``binders``
A list of binders. Each binder is an object with two fields:
- ``name``: A string that is the name to be bound, and
- ``definition``: A :ref:`JSON Cryptol expression <cryptol-json-expression>`.
``body``
A :ref:`JSON Cryptol expression <cryptol-json-expression>` in which the bound names may be used.
* The expression is a ``where``binding. The fields are:
*
``binders``
* A list of binders. Each binder is an object with two fields:
* ``name``: A string that is the name to be bound, and
* ``definition``A :ref:`JSON Cryptol expression <Expression>`.
``body``
A :ref:`JSON Cryptol expression <Expression>` in which the bound names may be used.
``call``
The expression is a function application. Further fields are:
- ``function``: A :ref:`JSON Cryptol expressions <cryptol-json-expression>`.
- ``arguments``: A JSON array of :ref:`JSON Cryptol expressions <cryptol-json-expression>`.
* The expression is a function application. Further fields are:
* ``function``: A :ref:`JSON Cryptol expression <Expression>`.
* ``arguments``: A JSON array of :ref:`JSON Cryptol expressions <Expression>`.
``instantiate``
The expression is a type application. Further fields are:
- ``generic``: The polymorphic expression to be instantiated
- ``arguments``: A JSON object in which keys are the names of type parameters and values are :ref:`JSON Cryptol types <cryptol-json-type>`.
* The expression is a type application. Further fields are:
* ``generic``: The polymorphic expression to be instantiated
* ``arguments``: A JSON object in which keys are the names of type parameters and values are :ref:`JSON Cryptol types <JSONSchema>`.
``integer modulo``
The expression is an integer with a modulus (the Cryptol ``Z`` type). Further fields are:
* The expression is an integer with a modulus (the Cryptol ``Z`` type). Further fields are:
* ``integer``: A JSON number, representing the integer
* ``modulus``: A JSON number, representing the modulus
- ``integer``: A JSON number, representing the integer
- ``modulus``: A JSON number, representing the modulus
.. _cryptol-json-type:
``variable``
The expression is a variable bound by the server. The field ``identifier`` contains the name of the variable.
.. _JSONSchema:
JSON Cryptol Types
------------------
~~~~~~~~~~~~~~~~~~
JSON representations of types are type schemas. A type schema has three fields:
JSON representations of types are type schemas. A type schema has
three fields:
``forall``
Contains an array of objects. Each object has two fields: ``name``
is the name of a type variable, and ``kind`` is its kind. There
are four kind formers: the string ``Type`` represents ordinary
datatypes, the string ``Num`` is the kind of numbers, and
``Prop`` is the kind of propositions. Arrow kinds are represented
by objects in which the field ``kind`` is the string ``arrow``,
and the fields ``from`` and ``to`` are the kinds on the left and
right side of the arrow, respectively.
Contains an array of objects. Each object has two fields: ``name`` is the name of a type variable, and ``kind`` is its kind. There are four kind formers: the string ``Type`` represents ordinary datatypes, the string ``Num`` is the kind of numbers, and ``Prop`` is the kind of propositions. Arrow kinds are represented by objects in which the field ``kind`` is the string ``arrow``, and the fields ``from`` and ``to`` are the kinds on the left and right side of the arrow, respectively.
``propositions``
A JSON array of the constraints in the type.
``type``
The type in which the variables from ``forall`` are in scope and
the constraints in ``propositions`` are in effect.
The type in which the variables from ``forall`` are in scope and the constraints in ``propositions`` are in effect.
Concrete Types
Methods
-------
check (command)
~~~~~~~~~~~~~~~
Tests a property against random values to give quick feedback.
Parameter fields
++++++++++++++++
``expression``
The predicate (i.e., function) to check; must be a monomorphic function with return type Bit.
``number of tests``
The number of random inputs to test the property with, or ``all`` to exhaustively check the property (defaults to ``100`` if not provided). If ``all`` is specified and the property's argument types are not sufficiently small, checking may take longer than you are willing to wait!
Return fields
+++++++++++++
``tests run``
The number of tests that were successfully run.
``tests possible``
The maximum number of possible tests.
``result``
The overall test result, represented as one of three string values:``pass`` (all tests succeeded), ``fail`` (a test evaluated to ``False``), or``error`` (an exception was raised during evaluation).
``arguments``
Only returned if the ``result`` is ``fail`` or ``error``. An array of JSON objects indicating the arguments passed to the property which triggered the failure or error. Each object has an ``expr`` field, which is an individual argument expression, and a ``type`` field, which is the type of the argument expression.
``error message``
Only returned if the ``result`` is ``error``. A human-readable representation of the exception that was raised during evaluation.
clear state (notification)
~~~~~~~~~~~~~~~~~~~~~~~~~~
Clear a particular state from the Cryptol server (making room for subsequent/unrelated states).
Parameter fields
++++++++++++++++
``state to clear``
The state to clear from the server to make room for other unrelated states.
Return fields
+++++++++++++
No return fields
clear all states (notification)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Clear all states from the Cryptol server (making room for subsequent/unrelated states).
Parameter fields
++++++++++++++++
No parameters
Return fields
+++++++++++++
No return fields
extend search path (command)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Extend the server's search path with the given paths.
Parameter fields
++++++++++++++++
``paths``
The paths to add to the search path.
Return fields
+++++++++++++
No return fields
load module (command)
~~~~~~~~~~~~~~~~~~~~~
Load the specified module (by name).
Parameter fields
++++++++++++++++
``module name``
Name of module to load.
Return fields
+++++++++++++
No return fields
load file (command)
~~~~~~~~~~~~~~~~~~~
Load the specified module (by file path).
Parameter fields
++++++++++++++++
``file``
File path of the module to load.
Return fields
+++++++++++++
No return fields
focused module (command)
~~~~~~~~~~~~~~~~~~~~~~~~
The 'current' module. Used to decide how to print names, for example.
Parameter fields
++++++++++++++++
No parameters
Return fields
+++++++++++++
``module``
The name of the focused module, which would be shown in the prompt in the Cryptol REPL, or ``null`` if there is no such focused module.
``parameterized``
A Boolean value indicating whether the focused module is parameterized. This field is only present when the module name is not ``null``.
evaluate expression (command)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Evaluate the Cryptol expression to a value.
Parameter fields
++++++++++++++++
``expression``
The expression to evaluate.
Return fields
+++++++++++++
``value``
A :ref:`JSON Cryptol expression <Expression>` that denotes the value
``type``
A:ref:`JSON Cryptol type <JSONSchema>` that denotes the result type
``type string``
A human-readable representation of the result type
call (command)
~~~~~~~~~~~~~~
Types are represented as JSON objects. The ``type`` field contains one of the following tags (represented as JSON strings):
Evaluate the result of calling a Cryptol function on one or more parameters.
``variable``
The type is a type variable. The remaining fields are ``name``,
which contains the variable's name, and ``kind``, which contains
its kind (represented as in the ``forall`` section). When providing
types to Cryptol, the ``kind`` field should be elided, and type synonyms
may be provided with arguments through an optional ``arguments`` field.
Parameter fields
++++++++++++++++
``record``
The type is a record type. The remaining field is ``fields``,
which contains a JSON object whose keys are the names of fields and
whose values are the fields' types.
``number``
The type is a number. The field ``value`` contains the number
itself.
``inf``
The type is the infinite number. There are no further fields.
``Bit``
The type is the bit type. There are no further fields.
``Integer``
The type is the integer type. There are no further fields.
``Rational``
The type is the rational number type. There are no further fields.
``Z``
The type is integers modulo another value. The field ``modulus``
contains the modulus, which is a type.
``bitvector``
The type is a bitvector. The field ``width`` contains the number
of bits, which is a type.
``sequence``
The type is a sequence. The field ``length`` contains the length
of the sequence (a type), and the field ``contents`` contains the
type of entries in the sequence.
``function``
The type is a function type. The fields ``domain`` and ``range``
contain the domain and range types.
The function being called.
``unit``
The type is the unit type. There are no further fields.
``arguments``
The arguments the function is being applied to.
``tuple``
The type is a tuple. The field ``contents`` is a JSON array
containing the types of the projections from the tuple.
Return fields
+++++++++++++
One of ``+``, ``-``, ``*``, ``/``, ``%``, ``^^``, ``width``, ``min``, ``max``, ``/^``, ``%^``, ``lengthFromThenTo``
The type is an application of the indicated type function. The
arguments are contained in the ``arguments`` field, as a JSON
array.
Propositions
~~~~~~~~~~~~
``value``
A :ref:`JSON Cryptol expression <Expression>` that denotes the value
Propositions/constraints have the key ``prop``, mapped to one of the
following tags:
``type``
A:ref:`JSON Cryptol type <JSONSchema>` that denotes the result type
``==``
Equality. The equated terms are in the ``left`` and ``right``
fields.
``type string``
A human-readable representation of the result type
``!=``
Inequality. The disequated terms are in the ``left`` and
``right`` fields.
``>=``
Greater than. The greater type is in the ``greater`` field and the
lesser type is in the ``lesser`` field.
visible names (command)
~~~~~~~~~~~~~~~~~~~~~~~
``fin``
Finitude. The finite type is in the ``subject`` field.
List the currently visible (i.e., in scope) names.
Parameter fields
++++++++++++++++
No parameters
Return fields
+++++++++++++
``name``
A human-readable representation of the name
``type string``
A human-readable representation of the name's type schema
``type``
A:ref:`JSON Cryptol type <JSONSchema>`
``documentation``
An optional field containing documentation string for the name, if it is documented
check type (command)
~~~~~~~~~~~~~~~~~~~~
Check and return the type of the given expression.
Parameter fields
++++++++++++++++
``expression``
Expression to type check.
Return fields
+++++++++++++
``type schema``
A :ref:`JSON Cryptol Type <JSONSchema>`
prove or satisfy (command)
~~~~~~~~~~~~~~~~~~~~~~~~~~
Find a value which satisfies the given predicate, or show that it is valid.(i.e., find a value which when passed as the argument produces true or show that for all possible arguments the predicate will produce true).
Parameter fields
++++++++++++++++
``prover``
The SMT solver to use to check for satisfiability. I.e., one of the following: ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``, .
``expression``
The function to check for validity, satisfiability, or safety depending on the specified value for ``query type``. For validity and satisfiability checks, the function must be a predicate (i.e., monomorphic function with return type Bit).
``result count``
How many satisfying results to search for; either a positive integer or ``all``. Only affects satisfiability checks.
``query type``
Whether to attempt to prove the predicate is true for all possible inputs (``prove``), find some inputs which make the predicate true (``sat``), or prove a function is safe (``safe``).
Return fields
+++++++++++++
``result``
A string (one of ``unsatisfiable``, ``invalid``, or ``satisfied``) indicating the result of checking for validity, satisfiability, or safety.
``counterexample type``
Only used if the ``result`` is ``invalid``.This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``.
``counterexample``
Only used if the ``result`` is ``invalid``.A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression.
``models``
Only used if the ``result`` is ``satisfied``.A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression.
``has``
The selector is in the ``selector`` field, the type that has this
selector is in the ``type`` field, and the type expected for the
projection is in the ``is`` field.
``Arith``, ``Cmp``, ``SignedCmp``, ``Zero``, ``Logic``
The type that has these operations defined is in the ``subject``
field.
``Literal``
The size is in the ``size`` field, and the type is in the
``subject`` field.
``True``
There are no further fields.
``And``
The conjuncts are in the ``left`` and ``right`` fields.

353
cryptol-remote-api/docs/old-Cryptol.rst Normal file
View File

@ -0,0 +1,353 @@
==================
Cryptol Evaluation
==================
All methods in this section additionally propagate server state in the
manner described in the prior section.
These methods may return :ref:`a variety of Cryptol errors
<cryptol-server-errors>`, with codes in the range of ``20000``-``29999``.
Options
=======
Many of the options that can be set using the ``:set`` command at the
Cryptol REPL can be provided as parameters to methods in this API. In
addition to the listed fields, every command accepts an optional
``options`` parameter. Its value should be an object, and may have
zero or more of the following fields:
- ``call stacks``: A Boolean that determines whether to track call stacks.
- ``output``: An object that contains further parameters to control strings generated by Cryptol (these are visible in e.g. error messages, but do not affect the structured data returned in the API):
+ ``ASCII``: A Boolean (default ``true``).
+ ``base``: What base to display numbers in (default ``10``).
+ ``prefix of infinite lengths``: How much of an infinite sequence to display (default ``5``.
+ ``floating point base``: What base to display floating point numbers in (default ``10``).
+ ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fpFormat`` in the REPL).
Module Management
=================
Changing Directories
--------------------
:Method name:
``change directory``
:Parameters:
- ``directory``: The new working directory, represented as a string.
Loading Modules
---------------
:Method name:
``load module``
:Parameters:
- ``module name``: The name of the Cryptol module to be loaded.
Loading Files
-------------
:Method name:
``load file``
:Parameters:
- ``file``: The name of the Cryptol source file to be loaded.
Module Context
--------------
:Method name:
``focused module``
:Parameters: none
:Return fields:
- ``module``: The name of the focused module, which would be shown in the
prompt in the Cryptol REPL, or ``null`` if there is no such focused module.
- ``parameterized``: A Boolean value indicating whether the focused module is
parameterized. This field is only present when the module name is not
``null``.
Evaluation and Typechecking
===========================
Evaluating Expressions
----------------------
This method evaluates a Cryptol expression. The type of the expression
needs to be fully-determined and finite - that is, functions and
infinite streams are not supported, and neither is polymorphism.
:Method name:
``evaluate expression``
:Parameters:
- ``expression``: The :ref:`JSON Cryptol expression <cryptol-json-expression>` to be evaluated
:Return fields:
- ``value``: A :ref:`JSON Cryptol expression <cryptol-json-expression>` that denotes the value
- ``type``: A :ref:`JSON Cryptol type <cryptol-json-type>` that denotes the result type
- ``type string``: A human-readable representation of the result type
Calling Functions
-----------------
Note: this method may be removed in the future, because its abilities
have been subsumed by ``evaluate expression``.
This method applies a Cryptol function to some arguments. The type of
the resulting expression needs to be fully-determined and finite -
that is, functions and infinite streams are not supported, and neither
is polymorphism.
:Method name:
``call``
:Parameters:
- ``function``: The name of a Cryptol function that is currently in scope
- ``arguments``: A list of arguments to the function, encoded as JSON
Cryptol expressions
:Return fields:
- ``value``: A :ref:`JSON Cryptol expression <cryptol-json-expression>` that denotes the value
- ``type``: A :ref:`JSON Cryptol type <cryptol-json-type>` that denotes the result type
- ``type string``: A human-readable representation of the result type
Visible Names
-------------
Return information about all names in scope.
:Method name:
``visible names``
:Parameters: none
:Return value:
A list of name information objects. Each name information object has the following
fields:
- ``name``: A human-readable representation of the name
- ``type string``: A human-readable representation of the name's type schema
- ``type``: A :ref:`JSON Cryptol type <cryptol-json-type>`
Some will additionally have the following field:
- ``documentation``: The documentation string for the name, if it is documented
Checking Types
--------------
Check the type of an expression.
:Method name:
``check type``
:Parameters:
- ``expression``: A :ref:`JSON Cryptol expression <cryptol-json-expression>` for which a type is desired.
:Return fields:
- ``type schema``: A :ref:`JSON Cryptol type <cryptol-json-type>`
SAT
---
This method is not yet ready for public consumption.
Terms and Types
===============
.. _cryptol-json-expression:
JSON Cryptol Expressions
------------------------
In the API, Cryptol expressions can be represented by the following:
JSON Booleans
Represent the corresponding Cryptol Booleans
JSON Integers
Cryptol integer literals, that can be used at a variety of types
JSON Strings
Cryptol concrete syntax
JSON Objects
Objects can represent a variety of Cryptol expressions. The field
``expression`` contains a tag that can be used to determine the
remaining fields.
The tag values in objects can be:
``bits``
The expression is a bitvector. Further fields are:
+ ``encoding``: Either the string ``base64`` or ``hex``, for base-64 or hexadecimal
representations of the bitvector
+ ``data``: A string containing the actual data
+ ``width``: An integer: the bit-width of the represented bit vector
``record``
The expression is a record. The field ``data`` is a JSON
object that maps record field names to :ref:`JSON Cryptol expressions <cryptol-json-expression>`.
``sequence``
The expression is a sequence. The field ``data`` contains a
JSON array of the elements of the sequence; each is a JSON Cryptol
expression.
``tuple``
The expression is a tuple. The field ``data`` contains a JSON
array of the elements of the tuple; each is a JSON Cryptol
expression.
``unit``
The expression is the unit constructor, and there are no further fields.
``let``
The expression is a ``where`` binding. The fields are:
``binders``
A list of binders. Each binder is an object with two fields:
- ``name``: A string that is the name to be bound, and
- ``definition``: A :ref:`JSON Cryptol expression <cryptol-json-expression>`.
``body``
A :ref:`JSON Cryptol expression <cryptol-json-expression>` in which the bound names may be used.
``call``
The expression is a function application. Further fields are:
- ``function``: A :ref:`JSON Cryptol expressions <cryptol-json-expression>`.
- ``arguments``: A JSON array of :ref:`JSON Cryptol expressions <cryptol-json-expression>`.
``instantiate``
The expression is a type application. Further fields are:
- ``generic``: The polymorphic expression to be instantiated
- ``arguments``: A JSON object in which keys are the names of type parameters and values are :ref:`JSON Cryptol types <cryptol-json-type>`.
``integer modulo``
The expression is an integer with a modulus (the Cryptol ``Z`` type). Further fields are:
- ``integer``: A JSON number, representing the integer
- ``modulus``: A JSON number, representing the modulus
.. _cryptol-json-type:
JSON Cryptol Types
------------------
JSON representations of types are type schemas. A type schema has
three fields:
``forall``
Contains an array of objects. Each object has two fields: ``name``
is the name of a type variable, and ``kind`` is its kind. There
are four kind formers: the string ``Type`` represents ordinary
datatypes, the string ``Num`` is the kind of numbers, and
``Prop`` is the kind of propositions. Arrow kinds are represented
by objects in which the field ``kind`` is the string ``arrow``,
and the fields ``from`` and ``to`` are the kinds on the left and
right side of the arrow, respectively.
``propositions``
A JSON array of the constraints in the type.
``type``
The type in which the variables from ``forall`` are in scope and
the constraints in ``propositions`` are in effect.
Concrete Types
~~~~~~~~~~~~~~
Types are represented as JSON objects. The ``type`` field contains one of the following tags (represented as JSON strings):
``variable``
The type is a type variable. The remaining fields are ``name``,
which contains the variable's name, and ``kind``, which contains
its kind (represented as in the ``forall`` section). When providing
types to Cryptol, the ``kind`` field should be elided, and type synonyms
may be provided with arguments through an optional ``arguments`` field.
``record``
The type is a record type. The remaining field is ``fields``,
which contains a JSON object whose keys are the names of fields and
whose values are the fields' types.
``number``
The type is a number. The field ``value`` contains the number
itself.
``inf``
The type is the infinite number. There are no further fields.
``Bit``
The type is the bit type. There are no further fields.
``Integer``
The type is the integer type. There are no further fields.
``Rational``
The type is the rational number type. There are no further fields.
``Z``
The type is integers modulo another value. The field ``modulus``
contains the modulus, which is a type.
``bitvector``
The type is a bitvector. The field ``width`` contains the number
of bits, which is a type.
``sequence``
The type is a sequence. The field ``length`` contains the length
of the sequence (a type), and the field ``contents`` contains the
type of entries in the sequence.
``function``
The type is a function type. The fields ``domain`` and ``range``
contain the domain and range types.
``unit``
The type is the unit type. There are no further fields.
``tuple``
The type is a tuple. The field ``contents`` is a JSON array
containing the types of the projections from the tuple.
One of ``+``, ``-``, ``*``, ``/``, ``%``, ``^^``, ``width``, ``min``, ``max``, ``/^``, ``%^``, ``lengthFromThenTo``
The type is an application of the indicated type function. The
arguments are contained in the ``arguments`` field, as a JSON
array.
Propositions
~~~~~~~~~~~~
Propositions/constraints have the key ``prop``, mapped to one of the
following tags:
``==``
Equality. The equated terms are in the ``left`` and ``right``
fields.
``!=``
Inequality. The disequated terms are in the ``left`` and
``right`` fields.
``>=``
Greater than. The greater type is in the ``greater`` field and the
lesser type is in the ``lesser`` field.
``fin``
Finitude. The finite type is in the ``subject`` field.
``has``
The selector is in the ``selector`` field, the type that has this
selector is in the ``type`` field, and the type expected for the
projection is in the ``is`` field.
``Arith``, ``Cmp``, ``SignedCmp``, ``Zero``, ``Logic``
The type that has these operations defined is in the ``subject``
field.
``Literal``
The size is in the ``size`` field, and the type is in the
``subject`` field.
``True``
There are no further fields.
``And``
The conjuncts are in the ``left`` and ``right`` fields.

3
cryptol-remote-api/python/cryptol/commands.py
View File

@ -11,6 +11,7 @@ import argo_client.interaction as argo
from argo_client.interaction import HasProtocolState
from . import solver
from .bitvector import BV
from .opaque import OpaqueValue
def extend_hex(string : str) -> str:
@ -49,6 +50,8 @@ def from_cryptol_arg(val : Any) -> Any:
else:
raise ValueError("Unknown encoding " + str(enc))
return BV(size, n)
elif tag == 'variable':
return OpaqueValue(str(val['identifier']))
else:
raise ValueError("Unknown expression tag " + tag)
else:

6
cryptol-remote-api/python/cryptol/cryptoltypes.py
View File

@ -5,6 +5,7 @@ import base64
from math import ceil
import BitVector #type: ignore
from .bitvector import BV
from .opaque import OpaqueValue
from typing import Any, Dict, Iterable, List, NoReturn, Optional, TypeVar, Union
@ -30,6 +31,7 @@ class CryptolLiteral(CryptolCode):
def __to_cryptol__(self, ty : CryptolType) -> Any:
return self._code
class CryptolApplication(CryptolCode):
def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None:
self._rator = rator
@ -163,6 +165,9 @@ class CryptolType:
'encoding': 'hex',
'width': val.size(), # N.B. original length, not padded
'data': val.hex()[2:]}
elif isinstance(val, OpaqueValue):
return {'expression': 'variable',
'identifier': val.identifier}
else:
raise TypeError("Unsupported value: " + str(val))
@ -407,6 +412,7 @@ class Record(CryptolType):
def __repr__(self) -> str:
return f"Record({self.fields!r})"
def to_type(t : Any) -> CryptolType:
if t['type'] == 'variable':
return Var(t['name'], to_kind(t['kind']))

28
cryptol-remote-api/python/cryptol/opaque.py Normal file
View File

@ -0,0 +1,28 @@
from typing import Any
class OpaqueValue():
"""A value from the Cryptol server which cannot be directly represented and/or
marshalled to an RPC client.
Note that as far as Python is concerned these values are only equal to
themselves. If a richer notion of equality is required then the server should
be consulted to compute the result."""
identifier : str
def __init__(self, identifier : str) -> None:
self.identifier = identifier
def __str__(self) -> str:
return self.identifier
def __repr__(self) -> str:
return f"Opaque({self.identifier!r})"
def __eq__(self, other : Any) -> bool:
if not isinstance(other, OpaqueValue):
return False
else:
return self.identifier == other.identifier
def __hash__(self) -> int:
return hash(self.identifier)

50
cryptol-remote-api/python/tests/cryptol/test-files/CplxQNewtype.cry Normal file
View File

@ -0,0 +1,50 @@
// This is a development of rational complex numbers
type Q = Rational
fortyTwo : Q
fortyTwo = 42
// Complex rational numbers in rectangular coordinates
newtype CplxQ =
{ real : Q, imag : Q }
embedQ : Q -> CplxQ
embedQ x = CplxQ{ real = x, imag = 0 }
cplxTwo : CplxQ
cplxTwo = embedQ 2
cplxForty : CplxQ
cplxForty = embedQ 40
cplxFortyTwo : CplxQ
cplxFortyTwo = embedQ 42
cplxAdd : CplxQ -> CplxQ -> CplxQ
cplxAdd x y = CplxQ { real = r, imag = i }
where
r = x.real + y.real
i = x.imag + y.imag
cplxMul : CplxQ -> CplxQ -> CplxQ
cplxMul x y = CplxQ { real = r, imag = i }
where
r = x.real * y.real - x.imag * y.imag
i = x.real * y.imag + x.imag * y.real
cplxEq : CplxQ -> CplxQ -> Bit
cplxEq x y = (x.real == y.real) && (x.imag == y.imag)
property cplxAddAssoc x y z =
cplxEq (cplxAdd (cplxAdd x y) z)
(cplxAdd x (cplxAdd y z))
property cplxMulAssoc x y z =
cplxEq (cplxMul (cplxMul x y) z)
(cplxMul x (cplxMul y z))
property cplxMulDistrib x y z =
cplxEq (cplxMul x (cplxAdd y z))
(cplxAdd (cplxMul x y) (cplxMul x z))

33
cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py Normal file
View File

@ -0,0 +1,33 @@
import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.bitvector import BV
class TestCplxQ(unittest.TestCase):
def test_CplxQ(self):
c = cryptol.connect(reset_server=True)
c.load_file(str(Path('tests','cryptol','test-files', 'CplxQNewtype.cry')))
forty_two = c.eval("fortyTwo").result()
cplx_forty_two1 = c.call("embedQ", forty_two).result()
cplx_forty_two2 = c.eval("CplxQ{ real = 42, imag = 0 }").result()
cplx_two = c.eval("cplxTwo").result()
cplx_forty = c.eval("cplxForty").result()
cplx_forty_two3 = c.call("cplxAdd", cplx_two, cplx_forty).result()
cplx_forty_two4 = c.eval("cplxMul (CplxQ{ real = 21, imag = 0 }) (CplxQ{ real = 2, imag = 0 })").result()
cplx_forty_two5 = c.eval("cplxAdd (CplxQ{ real = 41, imag = 0 }) (CplxQ{ real = 1, imag = 0 })").result()
cplx_forty_two6 = c.eval("CplxQ{ real = 42, imag = 0 }").result()
self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two2).result())
self.assertFalse(c.call("cplxEq", cplx_two, cplx_forty_two2).result())
self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two3).result())
self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two4).result())
self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two5).result())
self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two6).result())
if __name__ == "__main__":
unittest.main()

73
cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py
View File

@ -12,23 +12,24 @@ from distutils.spawn import find_executable
# cryptol_path = dir_path.joinpath('data')
# Test empty options
def do_test_options(c, state, options):
def do_test_options(test : unittest.TestCase, c, state, options):
id_opt = c.send_command("evaluate expression", {"state": state, "expression": "four", "options": options})
reply = c.wait_for_reply_to(id_opt)
assert('result' in reply)
assert('answer' in reply['result'])
assert('value' in reply['result']['answer'])
assert(reply['result']['answer']['value'] == {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'})
test.assertIn('result', reply)
test.assertIn('answer', reply['result'])
test.assertIn('value', reply['result']['answer'])
test.assertEqual(reply['result']['answer']['value'], {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'})
return reply['result']['state']
def do_test_instantiation(c, state, t, expected=None):
def do_test_instantiation(test : unittest.TestCase, c, state, t, expected=None):
if expected is None: expected = t
id_t = c.send_command("check type", {"state": state, "expression": {"expression": "instantiate", "generic": "id", "arguments": {"a": t}}})
reply = c.wait_for_reply_to(id_t)
assert('result' in reply)
assert('answer' in reply['result'])
assert('type schema' in reply['result']['answer'])
assert(reply['result']['answer']['type schema']['type']['domain'] == expected)
test.assertIn('result', reply)
test.assertIn('result', reply)
test.assertIn('answer', reply['result'])
test.assertIn('type schema', reply['result']['answer'])
test.assertEqual(reply['result']['answer']['type schema']['type']['domain'], expected)
return reply['result']['state']
class LowLevelCryptolApiTests(unittest.TestCase):
@ -119,27 +120,7 @@ class LowLevelCryptolApiTests(unittest.TestCase):
'unit':
{'expression': 'unit'}}})
state = reply['result']['state']
uid = c.send_command("evaluate expression",
{"state": state,
"expression": {"expression": "let",
"binders": [{"name": "theRecord", "definition": a_record}],
"body": {"expression": "tuple",
"data": [a_record, "theRecord"]}}})
reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply)
self.assertIn('answer', reply['result'])
self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply['result']['answer']['value'],
{'expression': 'tuple',
'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
'unit': {'expression': 'unit'}},
'expression': 'record'},
{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
'unit': {'expression': 'unit'}},
'expression': 'record'}]})
state = reply['result']['state']
uid = c.send_command("evaluate expression",
{"state": state,
"expression": {"expression": "sequence",
@ -161,8 +142,8 @@ class LowLevelCryptolApiTests(unittest.TestCase):
uid = c.send_command("evaluate expression",
{"state": state,
"expression": {"expression": "integer modulo",
"integer": 14,
"modulus": 42}})
"integer": 14,
"modulus": 42}})
reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply)
self.assertIn('answer', reply['result'])
@ -211,29 +192,29 @@ class LowLevelCryptolApiTests(unittest.TestCase):
self.assertEqual(reply['result']['answer']['value'], {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'})
state = reply['result']['state']
state = do_test_options(c, state, dict())
state = do_test_options(c, state, {"call stacks": True})
state = do_test_options(c, state, {"call stacks": False})
state = do_test_options(c, state, {"call stacks": False, "output": dict()})
state = do_test_options(c, state, {"call stacks": False, "output": {"ASCII": True}})
state = do_test_options(c, state, {"call stacks": False, "output": {"base": 16}})
state = do_test_options(c, state, {"call stacks": False, "output": {"prefix of infinite lengths": 3}})
state = do_test_options(self, c, state, dict())
state = do_test_options(self, c, state, {"call stacks": True})
state = do_test_options(self, c, state, {"call stacks": False})
state = do_test_options(self, c, state, {"call stacks": False, "output": dict()})
state = do_test_options(self, c, state, {"call stacks": False, "output": {"ASCII": True}})
state = do_test_options(self, c, state, {"call stacks": False, "output": {"base": 16}})
state = do_test_options(self, c, state, {"call stacks": False, "output": {"prefix of infinite lengths": 3}})
# These test both the type instantiation form and the serialization/deserialization of the types involved
state = do_test_instantiation(c, state, {"type": "Integer"})
state = do_test_instantiation(c, state, {"type": "record",
state = do_test_instantiation(self, c, state, {"type": "Integer"})
state = do_test_instantiation(self, c, state, {"type": "record",
"fields": {'a': {'type': 'Integer'},
'b': {'type': 'sequence', 'length': {'type': 'inf'}, 'contents': {'type': 'unit'}}}})
state = do_test_instantiation(c, state, {'type': 'sequence',
state = do_test_instantiation(self, c, state, {'type': 'sequence',
'length': {'type': 'number', 'value': 42},
'contents': {'type': 'Rational'}})
state = do_test_instantiation(c, state, {'type': 'bitvector',
state = do_test_instantiation(self, c, state, {'type': 'bitvector',
'width': {'type': 'number', 'value': 432}})
state = do_test_instantiation(c, state, {'type': 'variable',
state = do_test_instantiation(self, c, state, {'type': 'variable',
'name': 'Word8'},
{'type': 'bitvector',
'width': {'type': 'number', 'value': 8}})
state = do_test_instantiation(c, state, {'type': 'variable',
state = do_test_instantiation(self, c, state, {'type': 'variable',
'name': 'Twenty',
'arguments': [{'type': 'Z', 'modulus': {'type': 'number', 'value': 5}}]},
{ 'type': 'sequence',

53
cryptol-remote-api/run_rpc_tests.sh
View File

@ -1,54 +1,39 @@
#!/bin/bash
set -euo pipefail
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
pushd $DIR
cabal v2-build exe:cryptol-remote-api
cabal v2-build exe:cryptol-eval-server
pushd $DIR/python
NUM_FAILS=0
function run_test {
run_test() {
"$@"
if (( $? != 0 )); then NUM_FAILS=$(($NUM_FAILS+1)); fi
}
cabal-which() {
which $1 || cabal v2-exec which $1 || { echo "could not locate $1 executable" >&2 && exit 1; }
}
get_server() {
CRYPTOL_SERVER=$(cabal-which $1)
export CRYPTOL_SERVER
echo "Using server $CRYPTOL_SERVER"
}
echo "Setting up python environment for remote server clients..."
poetry install
echo "Typechecking code with mypy..."
run_test poetry run mypy cryptol/ tests/
export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api)
if [[ -x "$CRYPTOL_SERVER" ]]; then
echo "Running cryptol-remote-api tests..."
echo "Using server $CRYPTOL_SERVER"
run_test poetry run python -m unittest discover tests/cryptol
else
echo "could not find the cryptol-remote-api via `cabal v2-exec which`"
NUM_FAILS=$(($NUM_FAILS+1))
fi
get_server cryptol-remote-api
echo "Running cryptol-remote-api tests..."
run_test poetry run python -m unittest discover tests/cryptol
export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-eval-server)
if [[ -x "$CRYPTOL_SERVER" ]]; then
echo "Running cryptol-eval-server tests..."
echo "Using server $CRYPTOL_SERVER"
run_test poetry run python -m unittest discover tests/cryptol_eval
else
echo "could not find the cryptol-eval-server via `cabal v2-exec which`"
NUM_FAILS=$(($NUM_FAILS+1))
fi
popd
get_server cryptol-eval-server
echo "Running cryptol-eval-server tests..."
run_test poetry run python -m unittest discover tests/cryptol_eval
popd
if [ $NUM_FAILS -eq 0 ]
then
echo "All RPC tests passed"
exit 0
else
echo "Some RPC tests failed"
exit 1
fi

35
cryptol-remote-api/src/CryptolServer.hs
View File

@ -13,10 +13,11 @@ import Data.Containers.ListUtils (nubOrd)
import Data.Text (Text)
import Cryptol.Eval (EvalOpts(..))
import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv, ModuleInput(..))
import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv(..), ModuleInput(..))
import Cryptol.ModuleSystem.Env
(getLoadedModules, lmFilePath, lmFingerprint, meLoadedModules,
initialModuleEnv, meSearchPath, ModulePath(..))
(getLoadedModules, lmFilePath, lmFingerprint,
initialModuleEnv, ModulePath(..))
import Cryptol.ModuleSystem.Name (FreshM(..))
import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
import Cryptol.Parser.AST (ModName)
import Cryptol.TypeCheck( defaultSolverConfig )
@ -36,7 +37,7 @@ newtype CryptolNotification a = CryptolNotification { runCryptolNotification ::
command ::
forall params result.
(JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedParams params) =>
(JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedMethod params result) =>
Text ->
Doc.Block ->
(params -> CryptolCommand result) ->
@ -47,7 +48,7 @@ command name doc f = Argo.command name doc f'
notification ::
forall params.
(JSON.FromJSON params, Doc.DescribedParams params) =>
(JSON.FromJSON params, Doc.DescribedMethod params ()) =>
Text ->
Doc.Block ->
(params -> CryptolNotification ()) ->
@ -73,15 +74,19 @@ instance CryptolMethod CryptolNotification where
getModuleEnv :: CryptolCommand ModuleEnv
getModuleEnv = CryptolCommand $ const $ view moduleEnv <$> Argo.getState
getTCSolver :: CryptolCommand SMT.Solver
getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
setModuleEnv :: ModuleEnv -> CryptolCommand ()
setModuleEnv me =
CryptolCommand $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv me s)
runModuleCmd :: ModuleCmd a -> CryptolCommand a
runModuleCmd cmd =
modifyModuleEnv :: (ModuleEnv -> ModuleEnv) -> CryptolCommand ()
modifyModuleEnv f =
CryptolCommand $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv (f (view moduleEnv s)) s)
getTCSolver :: CryptolCommand SMT.Solver
getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
liftModuleCmd :: ModuleCmd a -> CryptolCommand a
liftModuleCmd cmd =
do Options callStacks evOpts <- getOptions
s <- CryptolCommand $ const Argo.getState
reader <- CryptolCommand $ const Argo.getFileReader
@ -129,6 +134,7 @@ moduleEnv = lens _moduleEnv (\v n -> v { _moduleEnv = n })
tcSolver :: Lens' ServerState SMT.Solver
tcSolver = lens _tcSolver (\v n -> v { _tcSolver = n })
initialState :: IO ServerState
initialState =
do modEnv <- initialModuleEnv
@ -140,7 +146,14 @@ extendSearchPath paths =
over moduleEnv $ \me -> me { meSearchPath = nubOrd $ paths ++ meSearchPath me }
instance FreshM CryptolCommand where
liftSupply f = do
serverState <- CryptolCommand $ const Argo.getState
let mEnv = view moduleEnv serverState
(res, supply') = f (meSupply $ mEnv)
mEnv' = mEnv { meSupply = supply' }
CryptolCommand $ const (Argo.modifyState $ set moduleEnv mEnv')
pure res
-- | Check that all of the modules loaded in the Cryptol environment
-- currently have fingerprints that match those when they were loaded.

21
cryptol-remote-api/src/CryptolServer/Call.hs
View File

@ -1,8 +1,10 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
module CryptolServer.Call
( Expression(..)
@ -16,9 +18,11 @@ module CryptolServer.Call
import qualified Argo.Doc as Doc
import Data.Aeson as JSON hiding (Encoding, Value, decode)
import qualified Data.Aeson as JSON
import Data.Typeable (Proxy(..), typeRep)
import CryptolServer
import CryptolServer.Data.Expression
import CryptolServer.Data.Type
import CryptolServer.EvalExpr (evalExpression')
callDescr :: Doc.Block
@ -42,10 +46,25 @@ instance FromJSON CallParams where
withObject "params for \"call\"" $
\o -> CallParams <$> o .: "function" <*> o .: "arguments"
instance Doc.DescribedParams CallParams where
instance Doc.DescribedMethod CallParams JSON.Value where
parameterFieldDescription =
[("function",
Doc.Paragraph [Doc.Text "The function being called."])
, ("arguments",
Doc.Paragraph [Doc.Text "The arguments the function is being applied to."])
]
resultFieldDescription =
[ ("value",
Doc.Paragraph [ Doc.Text "A "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
, Doc.Text " that denotes the value"
])
, ("type",
Doc.Paragraph [ Doc.Text " A"
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type"
, Doc.Text " that denotes the result type"
])
, ("type string",
Doc.Paragraph [Doc.Text "A human-readable representation of the result type"])
]

45
cryptol-remote-api/src/CryptolServer/Check.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
@ -35,13 +36,13 @@ import Cryptol.TypeCheck.Solve (defaultReplExpr)
import CryptolServer
( getTCSolver,
getModuleEnv,
runModuleCmd,
liftModuleCmd,
CryptolMethod(raise),
CryptolCommand )
import CryptolServer.Exceptions (evalPolyErr)
import CryptolServer.Data.Expression
( readBack, observe, getExpr, Expression )
import CryptolServer.Data.Type
( readBack, getExpr, Expression)
import CryptolServer.Data.Type ( JSONType(..) )
import Cryptol.Utils.PP (pretty)
checkDescr :: Doc.Block
@ -53,7 +54,7 @@ checkDescr =
check :: CheckParams -> CryptolCommand CheckResult
check (CheckParams jsonExpr cMode) =
do e <- getExpr jsonExpr
(_expr, ty, schema) <- runModuleCmd (CM.checkExpr e)
(_expr, ty, schema) <- liftModuleCmd (CM.checkExpr e)
-- TODO? validEvalContext expr, ty, schema
s <- getTCSolver
perhapsDef <- liftIO (defaultReplExpr s ty schema)
@ -65,7 +66,7 @@ check (CheckParams jsonExpr cMode) =
let theType = apSubst su (AST.sType schema)
tenv <- CEE.envTypes . deEnv . meDynEnv <$> getModuleEnv
let tval = CET.evalValType tenv theType
val <- runModuleCmd (CM.evalExpr checked)
val <- liftModuleCmd (CM.evalExpr checked)
pure (val,tval)
let (isExaustive, randomTestNum) = case cMode of
ExhaustiveCheckMode -> (True, 0)
@ -85,8 +86,10 @@ check (CheckParams jsonExpr cMode) =
convertTestArg :: (CET.TValue, CEC.Value) -> CryptolCommand (JSONType, Expression)
convertTestArg (t, v) = do
e <- observe $ readBack t v
return (JSONType mempty (CET.tValTy t), e)
me <- readBack t v
case me of
Nothing -> error $ "type is not convertable: " ++ (show t)
Just e -> return (JSONType mempty (CET.tValTy t), e)
convertTestResult ::
[CET.TValue] {- ^ Argument types -} ->
@ -166,7 +169,7 @@ instance FromJSON CheckParams where
Right n -> pure $ Just $ RandomCheckMode $ (toInteger :: Int -> Integer) n) v)
num Nothing = pure Nothing
instance Doc.DescribedParams CheckParams where
instance Doc.DescribedMethod CheckParams CheckResult where
parameterFieldDescription =
[ ("expression",
Doc.Paragraph [Doc.Text "The predicate (i.e., function) to check; "
@ -182,3 +185,29 @@ instance Doc.DescribedParams CheckParams where
, Doc.Text " sufficiently small, checking may take longer than you are willing to wait!"
])
]
resultFieldDescription =
[ ("tests run",
Doc.Paragraph [Doc.Text "The number of tests that were successfully run."])
, ("tests possible",
Doc.Paragraph [Doc.Text "The maximum number of possible tests."])
, ("result",
Doc.Paragraph [ Doc.Text "The overall test result, represented as one of three string values:"
, Doc.Literal "pass", Doc.Text " (all tests succeeded), "
, Doc.Literal "fail", Doc.Text " (a test evaluated to ", Doc.Literal "False", Doc.Text "), or"
, Doc.Literal "error", Doc.Text " (an exception was raised during evaluation)."
])
, ("arguments",
Doc.Paragraph [ Doc.Text "Only returned if the ", Doc.Literal "result"
, Doc.Text " is ", Doc.Literal "fail", Doc.Text " or ", Doc.Literal "error", Doc.Text ". "
, Doc.Text "An array of JSON objects indicating the arguments passed to the property "
, Doc.Text "which triggered the failure or error. Each object has an "
, Doc.Literal "expr", Doc.Text " field, which is an individual argument expression, and a "
, Doc.Literal "type", Doc.Text " field, which is the type of the argument expression."
])
, ("error message",
Doc.Paragraph [ Doc.Text "Only returned if the ", Doc.Literal "result"
, Doc.Text " is ", Doc.Literal "error", Doc.Text ". "
, Doc.Text "A human-readable representation of the exception that was raised during evaluation."
])
]

7
cryptol-remote-api/src/CryptolServer/ClearState.hs
View File

@ -1,3 +1,4 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.ClearState
( clearState
@ -20,8 +21,8 @@ instance JSON.FromJSON ClearStateParams where
JSON.withObject "params for \"clear state\"" $
\o -> ClearStateParams <$> o .: "state to clear"
instance Doc.DescribedParams ClearStateParams where
parameterFieldDescription =
instance Doc.DescribedMethod ClearStateParams () where
parameterFieldDescription =
[("state to clear",
Doc.Paragraph [Doc.Text "The state to clear from the server to make room for other unrelated states."])
]
@ -42,7 +43,7 @@ instance JSON.FromJSON ClearAllStatesParams where
JSON.withObject "params for \"clear all states\"" $
\_ -> pure ClearAllStatesParams
instance Doc.DescribedParams ClearAllStatesParams where
instance Doc.DescribedMethod ClearAllStatesParams () where
parameterFieldDescription = []
clearAllStatesDescr :: Doc.Block

518
cryptol-remote-api/src/CryptolServer/Data/Expression.hs
View File

@ -3,14 +3,16 @@
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
module CryptolServer.Data.Expression
( module CryptolServer.Data.Expression
) where
import Control.Applicative
import Control.Exception (throwIO)
import Control.Monad.IO.Class
import Data.Aeson as JSON hiding (Encoding, Value, decode)
import qualified Data.ByteString as BS
@ -24,13 +26,13 @@ import qualified Data.Scientific as Sc
import Data.Text (Text, pack)
import qualified Data.Text as T
import Data.Traversable
import Data.Typeable (Proxy(..), typeRep)
import qualified Data.Vector as V
import Data.Text.Encoding (encodeUtf8)
import Numeric (showHex)
import Cryptol.Backend.Monad
import Cryptol.Backend.Concrete hiding (Concrete)
import qualified Cryptol.Backend.Concrete as C
import qualified Cryptol.Eval.Concrete as Concrete
import Cryptol.Backend.SeqMap (enumerateSeqMap)
import Cryptol.Backend.WordValue (asWordVal)
@ -38,17 +40,25 @@ import Cryptol.Eval (evalSel)
import Cryptol.Eval.Concrete (Value)
import Cryptol.Eval.Type (TValue(..), tValTy)
import Cryptol.Eval.Value (GenValue(..))
import Cryptol.ModuleSystem (ModuleCmd, getPrimMap, evalDecls, renameType)
import Cryptol.ModuleSystem.Env (deNames,meDynEnv)
import Cryptol.ModuleSystem.Monad (runModuleM, interactive)
import qualified Cryptol.ModuleSystem.Base as Base
import qualified Cryptol.ModuleSystem.Renamer as R
import Cryptol.ModuleSystem.Name
(Name, mkDeclared, NameSource( UserName ), liftSupply, nameIdent)
import Cryptol.ModuleSystem.NamingEnv (singletonE, shadowing, namespaceMap)
import Cryptol.Parser
import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type,
ExportType(..))
import qualified Cryptol.Parser as CP
import qualified Cryptol.Parser.AST as CP
import Cryptol.Parser.Position (Located(..), emptyRange)
import Cryptol.Parser.Selector
import qualified Cryptol.TypeCheck.AST as TC
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)
import Argo
import qualified Argo.Doc as Doc
import CryptolServer
import CryptolServer.Exceptions
import CryptolServer.Data.Type
@ -82,8 +92,13 @@ instance JSON.ToJSON LetBinding where
, "definition" .= def
]
-- | Cryptol expressions which can be serialized into JSON and sent
-- to an RPC client.
data Expression =
Bit !Bool
Variable !Text
-- ^ Used when we need to send a result back to an RPC client which
-- cannot be cleanly represented syntactically.
| Bit !Bool
| Unit
| Num !Encoding !Text !Integer -- ^ data and bitwidth
| Record !(HashMap Text Expression)
@ -91,17 +106,27 @@ data Expression =
| Tuple ![Expression]
| Integer !Integer
| IntegerModulo !Integer !Integer -- ^ value, modulus
| Concrete !Text
| Concrete !Text -- ^ Concrete Cryptol syntax as a string -- the Cryptol parser
-- will establish it's meaning based on the current focus/context
| Let ![LetBinding] !Expression
| Application !Expression !(NonEmpty Expression)
| TypeApplication !Expression !TypeArguments
deriving (Eq, Show)
newtype TypeArguments = TypeArguments (Map Ident JSONPType)
deriving (Eq, Show) via Map Ident (Type PName)
deriving (Eq, Show) via Map Ident (CP.Type CP.PName)
data ExpressionTag =
TagNum | TagRecord | TagSequence | TagTuple | TagUnit | TagLet | TagApp | TagTypeApp | TagIntMod
data ExpressionTag
= TagNum
| TagRecord
| TagSequence
| TagTuple
| TagUnit
| TagLet
| TagApp
| TagTypeApp
| TagIntMod
| TagVariable
instance JSON.FromJSON ExpressionTag where
parseJSON =
@ -116,18 +141,20 @@ instance JSON.FromJSON ExpressionTag where
"call" -> pure TagApp
"instantiate" -> pure TagTypeApp
"integer modulo" -> pure TagIntMod
"variable" -> pure TagVariable
_ -> empty
instance JSON.ToJSON ExpressionTag where
toJSON TagNum = "bits"
toJSON TagRecord = "record"
toJSON TagSequence = "sequence"
toJSON TagTuple = "tuple"
toJSON TagUnit = "unit"
toJSON TagLet = "let"
toJSON TagApp = "call"
toJSON TagTypeApp = "instantiate"
toJSON TagIntMod = "integer modulo"
toJSON TagNum = "bits"
toJSON TagRecord = "record"
toJSON TagSequence = "sequence"
toJSON TagTuple = "tuple"
toJSON TagUnit = "unit"
toJSON TagLet = "let"
toJSON TagApp = "call"
toJSON TagTypeApp = "instantiate"
toJSON TagIntMod = "integer modulo"
toJSON TagVariable = "variable"
instance JSON.FromJSON TypeArguments where
parseJSON =
@ -182,6 +209,8 @@ instance JSON.FromJSON Expression where
TypeApplication <$> o .: "generic" <*> o .: "arguments"
TagIntMod ->
IntegerModulo <$> o .: "integer" <*> o .: "modulus"
TagVariable ->
Variable <$> o .: "identifier"
instance ToJSON Encoding where
toJSON Hex = String "hex"
@ -227,127 +256,279 @@ instance JSON.ToJSON Expression where
, "function" .= fun
, "arguments" .= args
]
toJSON (TypeApplication gen _args) =
-- It would be dead code to do anything here, as type
-- instantiations are not values. This code is called only as part
-- of translating values (e.g. from "evaluate expression"). So we
-- just fall through, rather than writing complicated code to
-- serialize Type PName that never gets called and just bitrots.
toJSON gen
toJSON (Variable nm) =
object [ "expression" .= TagVariable
, "identifier" .= toJSON nm
]
toJSON (TypeApplication _gen (TypeArguments _args)) =
-- Presumably this is dead code, since values are what are sent back to
-- the user and type applications won't appear there ever.
error "JSON conversion of type applications is not yet supported"
decode :: (Argo.Method m, Monad m) => Encoding -> Text -> m Integer
instance Doc.Described Expression where
typeName = "JSON Cryptol Expressions"
description =
[ Doc.Paragraph [Doc.Text "In the API, Cryptol expressions can be represented by the following:"]
, Doc.DescriptionList
[ (pure $ Doc.Text "JSON Booleans",
Doc.Paragraph [Doc.Text "Represent the corresponding Cryptol Booleans"])
, (pure $ Doc.Text "JSON Integers",
Doc.Paragraph [Doc.Text "Cryptol integer literals, that can be used at a variety of types"])
, (pure $ Doc.Text "JSON Strings",
Doc.Paragraph [Doc.Text "Cryptol concrete syntax"])
, (pure $ Doc.Text "JSON Objects",
Doc.Paragraph [ Doc.Text "Objects can represent a variety of Cryptol expressions. The field "
, Doc.Literal "expression"
, Doc.Text " contains a tag that can be used to determine the remaining fields."
])
]
, Doc.Paragraph [Doc.Text "The tag values in objects can be:"]
, Doc.DescriptionList
[ (pure $ Doc.Literal "bits",
Doc.BulletedList
[ Doc.Paragraph [Doc.Text "The expression is a bitvector. Further fields are:"]
, Doc.Paragraph [ Doc.Literal "encoding", Doc.Text ": Either the string "
, Doc.Literal "base64", Doc.Text " or ", Doc.Literal "hex"
, Doc.Text ", for base-64 or hexadecimal representations of the bitvector"
]
, Doc.Paragraph [Doc.Literal "data", Doc.Text ": A string containing the actual data"]
, Doc.Paragraph [Doc.Literal "width", Doc.Text ": An integer: the bit-width of the represented bit vector"]
])
, (pure $ Doc.Literal "record",
Doc.Paragraph [ Doc.Text "The expression is a record. The field "
, Doc.Literal "data", Doc.Text " is a JSON object that maps record field names to "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expressions"
, Doc.Text "."
])
, (pure $ Doc.Literal "sequence",
Doc.Paragraph [ Doc.Text "The expression is a sequence. The field "
, Doc.Literal "data"
, Doc.Text "contains a JSON array of the elements of the sequence; "
, Doc.Text "each is a JSON Cryptol expression."
])
, (pure $ Doc.Literal "tuple",
Doc.Paragraph [ Doc.Text "The expression is a tuple. The field "
, Doc.Literal "data"
, Doc.Text "contains a JSON array of the elements of the tuple; "
, Doc.Text "each is a JSON Cryptol expression."
])
, (pure $ Doc.Literal "unit",
Doc.Paragraph [Doc.Text "The expression is the unit constructor, and there are no further fields."])
, (pure $ Doc.Literal "let",
Doc.BulletedList
[ Doc.Paragraph [ Doc.Text "The expression is a ", Doc.Literal "where"
, Doc.Text "binding. The fields are:"
]
, Doc.DescriptionList
[ (pure $ Doc.Literal "binders",
Doc.BulletedList
[ Doc.Paragraph [Doc.Text "A list of binders. Each binder is an object with two fields:"]
, Doc.Paragraph [ Doc.Literal "name"
, Doc.Text ": A string that is the name to be bound, and"
]
, Doc.Paragraph [ Doc.Literal "definition"
, Doc.Text "A "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
, Doc.Text "."
]
])
, (pure $ Doc.Literal "body",
Doc.Paragraph [ Doc.Text "A "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
, Doc.Text " in which the bound names may be used."
])
]
])
, (pure $ Doc.Literal "call",
Doc.BulletedList
[ Doc.Paragraph [Doc.Text "The expression is a function application. Further fields are:"]
, Doc.Paragraph [ Doc.Literal "function", Doc.Text ": A "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
, Doc.Text "."
]
, Doc.Paragraph [ Doc.Literal "arguments", Doc.Text ": A JSON array of "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expressions"
, Doc.Text "."
]
])
, (pure $ Doc.Literal "instantiate",
Doc.BulletedList
[ Doc.Paragraph [Doc.Text "The expression is a type application. Further fields are:"]
, Doc.Paragraph [ Doc.Literal "generic"
, Doc.Text ": The polymorphic expression to be instantiated"
]
, Doc.Paragraph [ Doc.Literal "arguments"
, Doc.Text ": A JSON object in which keys are the names of type parameters and values are "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol types"
, Doc.Text "."
]
])
, (pure $ Doc.Literal "integer modulo",
Doc.BulletedList
[ Doc.Paragraph [ Doc.Text "The expression is an integer with a modulus (the Cryptol "
, Doc.Literal "Z", Doc.Text " type). Further fields are:"
]
, Doc.Paragraph [ Doc.Literal "integer"
, Doc.Text ": A JSON number, representing the integer"
]
, Doc.Paragraph [ Doc.Literal "modulus"
, Doc.Text ": A JSON number, representing the modulus"
]
])
, (pure $ Doc.Literal "variable",
Doc.Paragraph [ Doc.Text "The expression is a variable bound by the server. The field "
, Doc.Literal "identifier"
, Doc.Text " contains the name of the variable."
])
]
]
decode ::
(Argo.Method m, Monad m) =>
Encoding ->
Text ->
m Integer
decode Base64 txt =
let bytes = encodeUtf8 txt
in
case Base64.decode bytes of
Left err ->
Argo.raise (invalidBase64 bytes err)
Right decoded -> return $ bytesToInt decoded
Left err -> Argo.raise (invalidBase64 bytes err)
Right decoded -> pure $ bytesToInt decoded
decode Hex txt =
squish <$> traverse hexDigit (T.unpack txt)
squish <$> traverse (hexDigit Argo.raise) (T.unpack txt)
where
squish = foldl (\acc i -> (acc * 16) + i) 0
hexDigit :: (Argo.Method m, Monad m) => Num a => Char -> m a
hexDigit '0' = pure 0
hexDigit '1' = pure 1
hexDigit '2' = pure 2
hexDigit '3' = pure 3
hexDigit '4' = pure 4
hexDigit '5' = pure 5
hexDigit '6' = pure 6
hexDigit '7' = pure 7
hexDigit '8' = pure 8
hexDigit '9' = pure 9
hexDigit 'a' = pure 10
hexDigit 'A' = pure 10
hexDigit 'b' = pure 11
hexDigit 'B' = pure 11
hexDigit 'c' = pure 12
hexDigit 'C' = pure 12
hexDigit 'd' = pure 13
hexDigit 'D' = pure 13
hexDigit 'e' = pure 14
hexDigit 'E' = pure 14
hexDigit 'f' = pure 15
hexDigit 'F' = pure 15
hexDigit c = Argo.raise (invalidHex c)
hexDigit ::
(Monad m, Num a) =>
(forall b. JSONRPCException -> m b) ->
Char ->
m a
hexDigit raiseJSONErr =
\case
'0' -> pure 0
'1' -> pure 1
'2' -> pure 2
'3' -> pure 3
'4' -> pure 4
'5' -> pure 5
'6' -> pure 6
'7' -> pure 7
'8' -> pure 8
'9' -> pure 9
'a' -> pure 10
'A' -> pure 10
'b' -> pure 11
'B' -> pure 11
'c' -> pure 12
'C' -> pure 12
'd' -> pure 13
'D' -> pure 13
'e' -> pure 14
'E' -> pure 14
'f' -> pure 15
'F' -> pure 15
c -> raiseJSONErr (invalidHex c)
getExpr :: Expression -> CryptolCommand (Expr PName)
-- | Given a textual unqualified type name as `Text`, get the corresponding
-- `Name` for the type in the current module environment.
getTypeName ::
(Monad m) =>
R.NamingEnv ->
(forall a. ModuleCmd a -> m a) ->
Text ->
m Name
getTypeName nmEnv runModuleCmd ty =
runModuleCmd $ renameType nmEnv (CP.UnQual (mkIdent ty))
getCryptolType ::
(Monad m) =>
R.NamingEnv ->
(forall a. ModuleCmd a -> m a) ->
JSONPType ->
m (CP.Type Name)
getCryptolType nmEnv runModuleCmd (JSONPType rawTy) =
runModuleCmd $ \env -> runModuleM env $ interactive $
Base.rename interactiveName nmEnv (R.rename rawTy)
getExpr :: Expression -> CryptolCommand (CP.Expr CP.PName)
getExpr = CryptolCommand . const . getCryptolExpr
-- N.B., used in SAWServer as well, hence the more generic monad
getCryptolExpr :: (Argo.Method m, Monad m) => Expression -> m (Expr PName)
getCryptolExpr :: (Argo.Method m, Monad m) => Expression -> m (CP.Expr CP.PName)
getCryptolExpr (Variable nm) =
return $ CP.EVar $ CP.UnQual $ mkIdent nm
getCryptolExpr Unit =
return $
ETyped
(ETuple [])
(TTuple [])
CP.ETyped
(CP.ETuple [])
(CP.TTuple [])
getCryptolExpr (Bit b) =
return $
ETyped
(EVar (UnQual (mkIdent $ if b then "True" else "False")))
TBit
CP.ETyped
(CP.EVar (CP.UnQual (mkIdent $ if b then "True" else "False")))
CP.TBit
getCryptolExpr (Integer i) =
return $
ETyped
(ELit (ECNum i (DecLit (pack (show i)))))
(TUser (UnQual (mkIdent "Integer")) [])
CP.ETyped
(CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
(CP.TUser (CP.UnQual (mkIdent "Integer")) [])
getCryptolExpr (IntegerModulo i n) =
return $
ETyped
(ELit (ECNum i (DecLit (pack (show i)))))
(TUser (UnQual (mkIdent "Z")) [TNum n])
CP.ETyped
(CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
(CP.TUser (CP.UnQual (mkIdent "Z")) [CP.TNum n])
getCryptolExpr (Num enc txt w) =
do d <- decode enc txt
return $ ETyped
(ELit (ECNum d (DecLit txt)))
(TSeq (TNum w) TBit)
return $ CP.ETyped
(CP.ELit (CP.ECNum d (CP.DecLit txt)))
(CP.TSeq (CP.TNum w) CP.TBit)
getCryptolExpr (Record fields) =
fmap (ERecord . recordFromFields) $ for (HM.toList fields) $
fmap (CP.ERecord . recordFromFields) $ for (HM.toList fields) $
\(recName, spec) ->
(mkIdent recName,) . (emptyRange,) <$> getCryptolExpr spec
getCryptolExpr (Sequence elts) =
EList <$> traverse getCryptolExpr elts
CP.EList <$> traverse getCryptolExpr elts
getCryptolExpr (Tuple projs) =
ETuple <$> traverse getCryptolExpr projs
CP.ETuple <$> traverse getCryptolExpr projs
getCryptolExpr (Concrete syntax) =
case parseExpr syntax of
case CP.parseExpr syntax of
Left err ->
Argo.raise (cryptolParseErr syntax err)
Right e -> pure e
getCryptolExpr (Let binds body) =
EWhere <$> getCryptolExpr body <*> traverse mkBind binds
CP.EWhere <$> getCryptolExpr body <*> traverse mkBind binds
where
mkBind (LetBinding x rhs) =
DBind .
CP.DBind .
(\bindBody ->
Bind { bName = fakeLoc (UnQual (mkIdent x))
, bParams = []
, bDef = bindBody
, bSignature = Nothing
, bInfix = False
, bFixity = Nothing
, bPragmas = []
, bMono = True
, bDoc = Nothing
, bExport = Public
CP.Bind { CP.bName = fakeLoc (CP.UnQual (mkIdent x))
, CP.bParams = []
, CP.bDef = bindBody
, CP.bSignature = Nothing
, CP.bInfix = False
, CP.bFixity = Nothing
, CP.bPragmas = []
, CP.bMono = True
, CP.bDoc = Nothing
, CP.bExport = CP.Public
}) .
fakeLoc .
DExpr <$>
CP.DExpr <$>
getCryptolExpr rhs
fakeLoc = Located emptyRange
getCryptolExpr (Application fun (arg :| [])) =
EApp <$> getCryptolExpr fun <*> getCryptolExpr arg
CP.EApp <$> getCryptolExpr fun <*> getCryptolExpr arg
getCryptolExpr (Application fun (arg1 :| (arg : args))) =
getCryptolExpr (Application (Application fun (arg1 :| [])) (arg :| args))
getCryptolExpr (TypeApplication gen (TypeArguments args)) =
EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args))
CP.EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args))
where
inst (n, t) = NamedInst (Named (Located emptyRange n) (unJSONPType t))
inst (n, t) = CP.NamedInst (CP.Named (Located emptyRange n) (unJSONPType t))
-- TODO add tests that this is big-endian
-- | Interpret a ByteString as an Integer
@ -355,61 +536,140 @@ bytesToInt :: BS.ByteString -> Integer
bytesToInt bs =
BS.foldl' (\acc w -> (acc * 256) + toInteger w) 0 bs
readBack :: TValue -> Value -> Eval Expression
-- | Read back a typed value (if possible) into syntax which can be sent to an
-- RPC client. For some values which do not have a guaranteed syntactic
-- representation, a fresh variable will be generated and bound to
-- the value so the variable can instead be sent to the RPC client.
readBack :: TValue -> Value -> CryptolCommand (Maybe Expression)
readBack ty val =
case ty of
-- TODO, add actual support for newtypes
TVNewtype _u _ts _tfs -> liftIO $ throwIO (invalidType (tValTy ty))
TVRec tfs ->
Record . HM.fromList <$>
sequence [ do fv <- evalSel C.Concrete val (RecordSel f Nothing)
fa <- readBack t fv
return (identText f, fa)
| (f, t) <- canonicalFields tfs
]
TVRec tfs -> do
vals <- mapM readBackRecFld $ canonicalFields tfs
pure $ (Record . HM.fromList) <$> sequence vals
TVTuple [] ->
pure Unit
TVTuple ts ->
Tuple <$> sequence [ do v <- evalSel C.Concrete val (TupleSel n Nothing)
a <- readBack t v
return a
| (n, t) <- zip [0..] ts
]
pure $ Just Unit
TVTuple ts -> do
vals <- mapM readBackTupleFld $ zip [0..] ts
pure $ Tuple <$> sequence vals
TVBit ->
case val of
VBit b -> pure (Bit b)
VBit b -> pure $ Just $ Bit b
_ -> mismatchPanic
TVInteger ->
case val of
VInteger i -> pure (Integer i)
VInteger i -> pure $ Just $ Integer i
_ -> mismatchPanic
TVIntMod n ->
case val of
VInteger i -> pure (IntegerModulo i n)
VInteger i -> pure $ Just $ IntegerModulo i n
_ -> mismatchPanic
TVSeq len contents
| contents == TVBit
, VWord width wv <- val ->
do BV w v <- asWordVal C.Concrete wv
let hexStr = T.pack $ showHex v ""
let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1))
return $ Num Hex (T.justifyRight paddedLen '0' hexStr) w
| VSeq _l (enumerateSeqMap len -> vs) <- val ->
Sequence <$> mapM (>>= readBack contents) vs
TVSeq len elemTy
| elemTy == TVBit
, VWord width wv <- val -> do
Concrete.BV w v <- liftEval $ asWordVal Concrete.Concrete wv
let hexStr = T.pack $ showHex v ""
let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1))
pure $ Just $ Num Hex (T.justifyRight paddedLen '0' hexStr) w
| VSeq _l (enumerateSeqMap len -> mVals) <- val -> do
vals <- liftEval $ sequence mVals
es <- mapM (readBack elemTy) vals
pure $ Sequence <$> sequence es
other -> liftIO $ throwIO (invalidType (tValTy other))
_ -> do
-- The above cases are for types that can unambiguously be converted into
-- syntax; this case instead tries to essentially let-bind the value to a
-- fresh variable so we can send that to the RPC client instead. They
-- obviously won't be able to directly inspect the value, but they can
-- pass it to other functions/commands via a RPC.
mName <- bindValToFreshName (varName ty) ty val
case mName of
Nothing -> pure Nothing
Just name -> pure $ Just $ Variable name
where
mismatchPanic :: CryptolCommand (Maybe Expression)
mismatchPanic =
error $ "Internal error: readBack: value '" <>
show val <>
"' didn't match type '" <>
show (tValTy ty) <>
"'"
readBackRecFld :: (Ident, TValue) -> CryptolCommand (Maybe (Text, Expression))
readBackRecFld (fldId, fldTy) = do
fldVal <- liftEval $ evalSel Concrete.Concrete val (RecordSel fldId Nothing)
fldExpr <- readBack fldTy fldVal
pure $ (identText fldId,) <$> fldExpr
readBackTupleFld :: (Int, TValue) -> CryptolCommand (Maybe Expression)
readBackTupleFld (i, iTy) = do
iVal <- liftEval $ evalSel Concrete.Concrete val (TupleSel i Nothing)
readBack iTy iVal
varName :: TValue -> Text
varName =
\case
TVBit{} -> "bit"
TVInteger{} -> "integer"
TVFloat{} -> "float"
TVIntMod n -> "z" <> (T.pack $ show n)
TVRational{} -> "rational"
TVArray{} -> "array"
TVSeq{} -> "seq"
TVStream{} -> "stream"
TVTuple{} -> "tuple"
TVRec{} -> "record"
TVFun{} -> "fun"
TVNewtype nt _ _ -> identText $ nameIdent $ TC.ntName nt
TVAbstract{} -> "abstract"
observe :: Eval a -> CryptolCommand a
observe e = liftIO (runEval mempty e)
-- | Given a suggested `name` and a type and value, attempt to bind the value
-- to a freshly generated name in the current server environment. If successful,
-- the generated name will be of the form `CryptolServer'nameN` (where `N` is a
-- natural number) and the `FreshName` that is returned can be serialized into an
-- `Expression` and sent to an RPC client.
bindValToFreshName :: Text -> TValue -> Concrete.Value -> CryptolCommand (Maybe Text)
bindValToFreshName nameBase ty val = do
prims <- liftModuleCmd getPrimMap
mb <- liftEval (Concrete.toExpr prims ty val)
case mb of
Nothing -> return Nothing
Just expr -> do
(txt, name) <- genFresh
let schema = TC.Forall { TC.sVars = []
, TC.sProps = []
, TC.sType = tValTy ty
}
decl = TC.Decl { TC.dName = name
, TC.dSignature = schema
, TC.dDefinition = TC.DExpr expr
, TC.dPragmas = []
, TC.dInfix = False
, TC.dFixity = Nothing
, TC.dDoc = Nothing
}
liftModuleCmd (evalDecls [TC.NonRecursive decl])
modifyModuleEnv $ \me ->
let denv = meDynEnv me
in me {meDynEnv = denv { deNames = singletonE (CP.UnQual (mkIdent txt)) name `shadowing` deNames denv }}
return $ Just txt
where
genFresh :: CryptolCommand (Text, Name)
genFresh = do
valNS <- (namespaceMap NSValue) . deNames . meDynEnv <$> getModuleEnv
let txt = nextNewName valNS (Map.size valNS)
ident = mkIdent txt
mpath = TopModule interactiveName
name <- liftSupply (mkDeclared NSValue mpath UserName ident Nothing emptyRange)
pure (txt, name)
where nextNewName :: Map CP.PName [Name] -> Int -> Text
nextNewName ns n =
let txt = "CryptolServer'" <> nameBase <> (T.pack $ show n)
pname = CP.UnQual (mkIdent txt)
in if Map.member pname ns
then nextNewName ns (n + 1)
else txt
mkEApp :: Expr PName -> [Expr PName] -> Expr PName
mkEApp f args = foldl EApp f args
liftEval :: Eval a -> CryptolCommand a
liftEval e = liftIO (runEval mempty e)
mkEApp :: CP.Expr CP.PName -> [CP.Expr CP.PName] -> CP.Expr CP.PName
mkEApp f args = foldl CP.EApp f args

32
cryptol-remote-api/src/CryptolServer/Data/Type.hs
View File

@ -26,6 +26,8 @@ import Cryptol.Utils.Ident (mkIdent)
import Cryptol.Utils.PP (pp)
import Cryptol.Utils.RecordMap (canonicalFields)
import qualified Argo.Doc as Doc
newtype JSONSchema = JSONSchema Schema
@ -212,7 +214,7 @@ instance JSON.ToJSON JSONType where
]
convert (TUser _n _args def) = convert def
convert (TNewtype _nt _ts) =
error "JSON conversion of newtypes is not yet supported TODO"
JSON.object [ "type" .= T.pack "newtype" ]
convert (TRec fields) =
JSON.object
[ "type" .= T.pack "record"
@ -294,3 +296,31 @@ instance JSON.FromJSON JSONPType where
unaryPropF prop f o = unaryProp prop <$> typeField o f
binTC tc f1 f2 o = tc <$> typeField o f1 <*> typeField o f2
tyFun tf o = C.TUser (name tf) <$> typeListField o "arguments"
instance Doc.Described JSONSchema where
typeName = "JSON Cryptol Types"
description =
[ Doc.Paragraph [Doc.Text "JSON representations of types are type schemas. A type schema has three fields:"]
, Doc.DescriptionList
[ (pure $ Doc.Literal "forall",
Doc.Paragraph [ Doc.Text "Contains an array of objects. Each object has two fields: "
, Doc.Literal "name", Doc.Text " is the name of a type variable, and "
, Doc.Literal "kind", Doc.Text " is its kind. There are four kind formers: the string "
, Doc.Literal "Type", Doc.Text " represents ordinary datatypes, the string "
, Doc.Literal "Num", Doc.Text " is the kind of numbers, and "
, Doc.Literal "Prop", Doc.Text " is the kind of propositions. "
, Doc.Text "Arrow kinds are represented by objects in which the field "
, Doc.Literal "kind", Doc.Text " is the string "
, Doc.Literal "arrow", Doc.Text ", and the fields "
, Doc.Literal "from", Doc.Text " and ", Doc.Literal "to"
, Doc.Text " are the kinds on the left and right side of the arrow, respectively."
])
, (pure $ Doc.Literal "propositions",
Doc.Paragraph [Doc.Text "A JSON array of the constraints in the type."])
, (pure $ Doc.Literal "type",
Doc.Paragraph [ Doc.Text "The type in which the variables from "
, Doc.Literal "forall", Doc.Text " are in scope and the constraints in "
, Doc.Literal "propositions", Doc.Text " are in effect."
])
]
]

74
cryptol-remote-api/src/CryptolServer/EvalExpr.hs
View File

@ -1,4 +1,6 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module CryptolServer.EvalExpr
( evalExpression
, evalExpressionDescr
@ -7,17 +9,18 @@ module CryptolServer.EvalExpr
) where
import qualified Argo.Doc as Doc
import Control.Exception (throwIO)
import Control.Monad.IO.Class
import Data.Aeson as JSON
import Data.Typeable (Proxy(..), typeRep)
import Cryptol.ModuleSystem (checkExpr, evalExpr)
import Cryptol.ModuleSystem (evalExpr, checkExpr)
import Cryptol.ModuleSystem.Env (deEnv,meDynEnv)
import Cryptol.TypeCheck.Solve (defaultReplExpr)
import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
import Cryptol.TypeCheck.Type (Schema(..))
import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Name (PName)
import Cryptol.Utils.PP (pretty)
import qualified Cryptol.Eval.Env as E
import qualified Cryptol.Eval.Type as E
@ -36,30 +39,32 @@ evalExpression (EvalExprParams jsonExpr) =
do e <- getExpr jsonExpr
evalExpression' e
evalExpression' :: P.Expr PName -> CryptolCommand JSON.Value
evalExpression' e =
do (_expr, ty, schema) <- runModuleCmd (checkExpr e)
-- TODO: see Cryptol REPL for how to check whether we
-- can actually evaluate things, which we can't do in
-- a parameterized module
s <- getTCSolver
perhapsDef <- liftIO (defaultReplExpr s ty schema)
case perhapsDef of
Nothing ->
raise (evalPolyErr schema)
Just (tys, checked) ->
do -- TODO: warnDefaults here
let su = listParamSubst tys
let theType = apSubst su (sType schema)
tenv <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv
let tval = E.evalValType tenv theType
res <- runModuleCmd (evalExpr checked)
val <- observe $ readBack tval res
return (JSON.object [ "value" .= val
, "type string" .= pretty theType
, "type" .= JSONSchema (Forall [] [] theType)
])
evalExpression' :: P.Expr P.PName -> CryptolCommand JSON.Value
evalExpression' e = do
(_expr, ty, schema) <- liftModuleCmd (checkExpr e)
-- TODO: see Cryptol REPL for how to check whether we
-- can actually evaluate things, which we can't do in
-- a parameterized module
s <- getTCSolver
perhapsDef <- liftIO (defaultReplExpr s ty schema)
case perhapsDef of
Nothing ->
raise (evalPolyErr schema)
Just (tys, checked) ->
do -- TODO: warnDefaults here
let su = listParamSubst tys
let theType = apSubst su (sType schema)
tenv <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv
let tval = E.evalValType tenv theType
val <- liftModuleCmd (evalExpr checked)
mExpr<- readBack tval val
case mExpr of
Just expr ->
pure $ JSON.object [ "value" .= expr
, "type string" .= pretty theType
, "type" .= JSONSchema (Forall [] [] theType)
]
Nothing -> liftIO $ throwIO (invalidType theType)
newtype EvalExprParams =
EvalExprParams Expression
@ -68,8 +73,23 @@ instance JSON.FromJSON EvalExprParams where
JSON.withObject "params for \"evaluate expression\"" $
\o -> EvalExprParams <$> o .: "expression"
instance Doc.DescribedParams EvalExprParams where
instance Doc.DescribedMethod EvalExprParams JSON.Value where
parameterFieldDescription =
[("expression",
Doc.Paragraph [Doc.Text "The expression to evaluate."])
]
resultFieldDescription =
[ ("value",
Doc.Paragraph [ Doc.Text "A "
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression"
, Doc.Text " that denotes the value"
])
, ("type",
Doc.Paragraph [ Doc.Text " A"
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type"
, Doc.Text " that denotes the result type"
])
, ("type string",
Doc.Paragraph [Doc.Text "A human-readable representation of the result type"])
]

4
cryptol-remote-api/src/CryptolServer/Exceptions.hs
View File

@ -17,6 +17,7 @@ import qualified Data.Text as Text
import qualified Data.Vector as Vector
import Cryptol.ModuleSystem (ModuleError(..), ModuleWarning(..))
import Cryptol.ModuleSystem.Name as CM
import Cryptol.Utils.PP (pretty, PP)
import Data.Aeson hiding (Encoding, Value, decode)
@ -26,7 +27,6 @@ import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.HashMap.Strict as HashMap
import Cryptol.ModuleSystem.Name (Name)
import Cryptol.Parser
import qualified Cryptol.TypeCheck.Type as TC
@ -170,7 +170,7 @@ unwantedDefaults defs =
[ jsonTypeAndString ty <> HashMap.fromList ["parameter" .= pretty param]
| (param, ty) <- defs ] ]))
evalInParamMod :: [Cryptol.ModuleSystem.Name.Name] -> JSONRPCException
evalInParamMod :: [CM.Name] -> JSONRPCException
evalInParamMod mods =
makeJSONRPCException
20220 "Can't evaluate Cryptol in a parameterized module."

3
cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs
View File

@ -1,3 +1,4 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.ExtendSearchPath
( extSearchPath
@ -31,7 +32,7 @@ instance FromJSON ExtendSearchPathParams where
withObject "params for \"extend search path\"" $
\o -> ExtendSearchPathParams <$> o .: "paths"
instance Doc.DescribedParams ExtendSearchPathParams where
instance Doc.DescribedMethod ExtendSearchPathParams () where
parameterFieldDescription =
[("paths",
Doc.Paragraph [Doc.Text "The paths to add to the search path."])

16
cryptol-remote-api/src/CryptolServer/FocusedModule.hs
View File

@ -1,3 +1,4 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.FocusedModule
( focusedModule
@ -36,5 +37,18 @@ data FocusedModParams = FocusedModParams
instance JSON.FromJSON FocusedModParams where
parseJSON _ = pure FocusedModParams
instance Doc.DescribedParams FocusedModParams where
instance Doc.DescribedMethod FocusedModParams JSON.Value where
parameterFieldDescription = []
resultFieldDescription =
[ ("module",
Doc.Paragraph [ Doc.Text "The name of the focused module, which would be shown in the "
, Doc.Text "prompt in the Cryptol REPL, or "
, Doc.Literal "null", Doc.Text " if there is no such focused module."
])
, ("parameterized",
Doc.Paragraph [ Doc.Text "A Boolean value indicating whether the focused module is "
, Doc.Text "parameterized. This field is only present when the module name is not "
, Doc.Literal "null", Doc.Text "."
])
]

9
cryptol-remote-api/src/CryptolServer/LoadModule.hs
View File

@ -1,3 +1,4 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.LoadModule
( loadFile
@ -25,7 +26,7 @@ loadFileDescr = Doc.Paragraph [Doc.Text "Load the specified module (by file path
loadFile :: LoadFileParams -> CryptolCommand ()
loadFile (LoadFileParams fn) =
void $ runModuleCmd (loadModuleByPath fn)
void $ liftModuleCmd (loadModuleByPath fn)
newtype LoadFileParams
= LoadFileParams FilePath
@ -36,7 +37,7 @@ instance JSON.FromJSON LoadFileParams where
\o -> LoadFileParams <$> o .: "file"
instance Doc.DescribedParams LoadFileParams where
instance Doc.DescribedMethod LoadFileParams () where
parameterFieldDescription =
[("file",
Doc.Paragraph [Doc.Text "File path of the module to load."])
@ -49,7 +50,7 @@ loadModuleDescr = Doc.Paragraph [Doc.Text "Load the specified module (by name)."
loadModule :: LoadModuleParams -> CryptolCommand ()
loadModule (LoadModuleParams mn) =
void $ runModuleCmd (loadModuleByName mn)
void $ liftModuleCmd (loadModuleByName mn)
newtype JSONModuleName
= JSONModuleName { unJSONModName :: ModName }
@ -70,7 +71,7 @@ instance JSON.FromJSON LoadModuleParams where
JSON.withObject "params for \"load module\"" $
\o -> LoadModuleParams . unJSONModName <$> o .: "module name"
instance Doc.DescribedParams LoadModuleParams where
instance Doc.DescribedMethod LoadModuleParams () where
parameterFieldDescription =
[("module name",
Doc.Paragraph [Doc.Text "Name of module to load."])

19
cryptol-remote-api/src/CryptolServer/Names.hs
View File

@ -1,6 +1,9 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module CryptolServer.Names
( visibleNames
, visibleNamesDescr
@ -12,6 +15,7 @@ import Data.Aeson ((.=))
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Text (unpack)
import Data.Typeable (Proxy(..), typeRep)
import Cryptol.Parser.Name (PName(..))
import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv)
@ -31,9 +35,22 @@ data VisibleNamesParams = VisibleNamesParams
instance JSON.FromJSON VisibleNamesParams where
parseJSON _ = pure VisibleNamesParams
instance Doc.DescribedParams VisibleNamesParams where
instance Doc.DescribedMethod VisibleNamesParams [NameInfo] where
parameterFieldDescription = []
resultFieldDescription =
[ ("name",
Doc.Paragraph [Doc.Text "A human-readable representation of the name"])
, ("type string",
Doc.Paragraph [Doc.Text "A human-readable representation of the name's type schema"])
, ("type",
Doc.Paragraph [ Doc.Text " A"
, Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type"
])
, ("documentation",
Doc.Paragraph [Doc.Text "An optional field containing documentation string for the name, if it is documented"])
]
visibleNamesDescr :: Doc.Block
visibleNamesDescr =
Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) names."]

8
cryptol-remote-api/src/CryptolServer/Options.hs
View File

@ -1,8 +1,11 @@
{-# OPTIONS_GHC -fno-warn-type-defaults -Wno-missing-deriving-strategies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module CryptolServer.Options (Options(..), WithOptions(..)) where
import qualified Argo.Doc as Doc
@ -73,8 +76,9 @@ instance FromJSON Options where
data WithOptions a = WithOptions Options a
deriving Functor
instance forall params . Doc.DescribedParams params => Doc.DescribedParams (WithOptions params) where
parameterFieldDescription = (Doc.parameterFieldDescription @params)
instance forall params result . Doc.DescribedMethod params result => Doc.DescribedMethod (WithOptions params) result where
parameterFieldDescription = Doc.parameterFieldDescription @params
resultFieldDescription = Doc.resultFieldDescription @params @result
instance FromJSON a => FromJSON (WithOptions a) where
parseJSON = withObject "parameters with options" $

45
cryptol-remote-api/src/CryptolServer/Sat.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
@ -44,7 +45,7 @@ proveSatDescr =
proveSat :: ProveSatParams -> CryptolCommand ProveSatResult
proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
do e <- getExpr jsonExpr
(_expr, ty, schema) <- runModuleCmd (checkExpr e)
(_expr, ty, schema) <- liftModuleCmd (checkExpr e)
-- TODO validEvalContext expr, ty, schema
me <- getModuleEnv
let decls = deDecls (meDynEnv me)
@ -72,7 +73,7 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
sbvCfg <- liftIO (setupProver name) >>= \case
Left msg -> error msg
Right (_ws, sbvCfg) -> return sbvCfg
(_firstProver, res) <- runModuleCmd $ satProve sbvCfg cmd
(_firstProver, res) <- liftModuleCmd $ satProve sbvCfg cmd
_stats <- liftIO (readIORef timing)
case res of
ProverError msg -> raise (proverError msg)
@ -86,9 +87,11 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
satResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)]
satResult es = traverse result es
result (t, _, v) =
do e <- observe $ readBack t v
return (JSONType mempty (tValTy t), e)
result (t, _, v) = do
me <- readBack t v
case me of
Nothing -> error $ "type is not convertable: " ++ (show t)
Just e -> pure (JSONType mempty (tValTy t), e)
data ProveSatResult
= Unsatisfiable
@ -168,7 +171,7 @@ instance FromJSON ProveSatParams where
Right int -> pure (SomeSat int)) v)
instance Doc.DescribedParams ProveSatParams where
instance Doc.DescribedMethod ProveSatParams ProveSatResult where
parameterFieldDescription =
[("prover",
Doc.Paragraph ([Doc.Text "The SMT solver to use to check for satisfiability. I.e., one of the following: "]
@ -195,3 +198,33 @@ instance Doc.DescribedParams ProveSatParams where
]
)
]
resultFieldDescription =
[ ("result",
Doc.Paragraph [ Doc.Text "A string (one of "
, Doc.Literal "unsatisfiable", Doc.Text ", "
, Doc.Literal "invalid", Doc.Text ", or "
, Doc.Literal "satisfied"
, Doc.Text ") indicating the result of checking for validity, satisfiability, or safety."
])
, ("counterexample type",
Doc.Paragraph $ onlyIfResultIs "invalid" ++
[ Doc.Text "This describes the variety of counterexample that was produced. This can be either "
, Doc.Literal "safety violation", Doc.Text " or ", Doc.Literal "predicate falsified", Doc.Text "."
])
, ("counterexample",
Doc.Paragraph $ onlyIfResultIs "invalid" ++
[ Doc.Text "A list of objects where each object has an "
, Doc.Literal "expr", Doc.Text "field, indicating a counterexample expression, and a "
, Doc.Literal "type", Doc.Text "field, indicating the type of the expression."
])
, ("models",
Doc.Paragraph $ onlyIfResultIs "satisfied" ++
[ Doc.Text "A list of list of objects where each object has an "
, Doc.Literal "expr", Doc.Text "field, indicating a expression in a model, and a "
, Doc.Literal "type", Doc.Text "field, indicating the type of the expression."
])
]
where
onlyIfResultIs val = [ Doc.Text "Only used if the " , Doc.Literal "result"
, Doc.Text " is ", Doc.Literal val, Doc.Text "." ]

25
cryptol-remote-api/src/CryptolServer/TypeCheck.hs
View File

@ -1,4 +1,6 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module CryptolServer.TypeCheck
( checkType
, checkTypeDescr
@ -9,11 +11,11 @@ import qualified Argo.Doc as Doc
--import Control.Lens hiding ((.=))
import Data.Aeson as JSON
import Data.Typeable
import Cryptol.ModuleSystem (checkExpr)
import CryptolServer
import CryptolServer.Exceptions
import CryptolServer.Data.Expression
import CryptolServer.Data.Type
@ -22,14 +24,10 @@ checkTypeDescr =
Doc.Paragraph [Doc.Text "Check and return the type of the given expression."]
checkType :: TypeCheckParams -> CryptolCommand JSON.Value
checkType (TypeCheckParams e) =
do e' <- getExpr e
(_expr, _ty, schema) <- runModuleCmd (checkExpr e')
return (JSON.object [ "type schema" .= JSONSchema schema ])
where
-- FIXME: Why is this check not being used?
_noDefaults [] = return ()
_noDefaults xs@(_:_) = raise (unwantedDefaults xs)
checkType (TypeCheckParams e) = do
e' <- getExpr e
(_expr, _ty, schema) <- liftModuleCmd (checkExpr e')
return (JSON.object [ "type schema" .= JSONSchema schema ])
newtype TypeCheckParams =
TypeCheckParams Expression
@ -39,8 +37,13 @@ instance JSON.FromJSON TypeCheckParams where
JSON.withObject "params for \"check type\"" $
\o -> TypeCheckParams <$> o .: "expression"
instance Doc.DescribedParams TypeCheckParams where
instance Doc.DescribedMethod TypeCheckParams JSON.Value where
parameterFieldDescription =
[("expression",
Doc.Paragraph [Doc.Text "Expression to type check."])
]
resultFieldDescription =
[("type schema",
Doc.Paragraph [Doc.Text "A ", Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol Type"])
]

2
deps/argo vendored

@ -1 +1 @@
Subproject commit 1040dc26d142f13ff8ed6617ff5212f476b78c45
Subproject commit c733718138c10c70c6e690d4a2de83a7b07e6cc9

47
src/Cryptol/Backend/Monad.hs
View File

@ -63,12 +63,33 @@ ready a = Ready a
-- | The type of dynamic call stacks for the interpreter.
-- New frames are pushed onto the right side of the sequence.
type CallStack = Seq (Name, Range)
data CallStack
= EmptyCallStack
| CombineCallStacks !CallStack !CallStack
| PushCallFrame !Name !Range !CallStack
instance Semigroup CallStack where
(<>) = CombineCallStacks
instance Monoid CallStack where
mempty = EmptyCallStack
type CallStack' = Seq (Name, Range)
evalCallStack :: CallStack -> CallStack'
evalCallStack stk =
case stk of
EmptyCallStack -> mempty
CombineCallStacks appstk fnstk -> combineCallStacks' (evalCallStack appstk) (evalCallStack fnstk)
PushCallFrame n r stk1 -> pushCallFrame' n r (evalCallStack stk1)
-- | Pretty print a call stack with each call frame on a separate
-- line, with most recent call frames at the top.
displayCallStack :: CallStack -> Doc
displayCallStack = vcat . map f . toList . Seq.reverse
displayCallStack = displayCallStack' . evalCallStack
displayCallStack' :: CallStack' -> Doc
displayCallStack' = vcat . map f . toList . Seq.reverse
where
f (nm,rng)
| rng == emptyRange = pp nm
@ -92,7 +113,15 @@ combineCallStacks ::
CallStack {- ^ call stack of the application context -} ->
CallStack {- ^ call stack of the function being applied -} ->
CallStack
combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
combineCallStacks appstk EmptyCallStack = appstk
combineCallStacks EmptyCallStack fnstk = fnstk
combineCallStacks appstk fnstk = CombineCallStacks appstk fnstk
combineCallStacks' ::
CallStack' {- ^ call stack of the application context -} ->
CallStack' {- ^ call stack of the function being applied -} ->
CallStack'
combineCallStacks' appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
where
dropCommonPrefix _ Seq.Empty = Seq.Empty
dropCommonPrefix Seq.Empty fs = fs
@ -102,9 +131,12 @@ combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
-- | Add a call frame to the top of a call stack
pushCallFrame :: Name -> Range -> CallStack -> CallStack
pushCallFrame nm rng stk@( _ Seq.:|> (nm',rng'))
pushCallFrame nm rng stk = PushCallFrame nm rng stk
pushCallFrame' :: Name -> Range -> CallStack' -> CallStack'
pushCallFrame' nm rng stk@( _ Seq.:|> (nm',rng'))
| nm == nm', rng == rng' = stk
pushCallFrame nm rng stk = stk Seq.:|> (nm,rng)
pushCallFrame' nm rng stk = stk Seq.:|> (nm,rng)
-- | The monad for Cryptol evaluation.
@ -417,11 +449,12 @@ data EvalErrorEx =
deriving Typeable
instance PP EvalErrorEx where
ppPrec _ (EvalErrorEx stk ex) = vcat ([ pp ex ] ++ callStk)
ppPrec _ (EvalErrorEx stk0 ex) = vcat ([ pp ex ] ++ callStk)
where
stk = evalCallStack stk0
callStk | Seq.null stk = []
| otherwise = [ text "-- Backtrace --", displayCallStack stk ]
| otherwise = [ text "-- Backtrace --", displayCallStack' stk ]
instance Show EvalErrorEx where
show = show . pp

2
src/Cryptol/REPL/Command.hs
View File

@ -1245,7 +1245,7 @@ helpCmd cmd
M.Parameter -> rPutStrLn "// No documentation is available."
showModHelp env disp x =
showModHelp _env disp x =
rPrint $ runDoc disp $ vcat [ "`" <> pp x <> "` is a module." ]
-- XXX: show doc. if any