GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-16 09:20:24 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into ghc9

Browse Source
This commit is contained in:
Ryan Scott 2022-01-12 09:33:24 -05:00
commit 644d33bf1f
264 changed files with 27902 additions and 2166 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

98
.github/ci.sh vendored
View File

@ -2,13 +2,28 @@
set -xEeuo pipefail
[[ "$RUNNER_OS" == 'Windows' ]] && IS_WIN=true || IS_WIN=false
BIN=bin
BIN=${PWD}/bin
EXT=""
$IS_WIN && EXT=".exe"
mkdir -p "$BIN"
is_exe() { [[ -x "$1/$2$EXT" ]] || command -v "$2" > /dev/null 2>&1; }
# The deps() function is primarily used for producing debug output to
# the CI logging files. For each platform, it will indicate which
# shared libraries are needed and if they are present or not. The
# '|| true' is used because statically linked binaries will cause
# ldd (and possibly otool) to exit with a non-zero status.
deps() {
case "$RUNNER_OS" in
Linux) ldd $1 || true ;;
macOS) otool -L $1 || true ;;
Windows) ldd $1 || true ;;
esac
}
# Finds the cabal-built '$1' executable and copies it to the '$2'
# directory.
extract_exe() {
exe="$(cabal v2-exec which "$1$EXT")"
name="$(basename "$exe")"
@ -45,63 +60,6 @@ setup_dist_bins() {
strip dist/bin/cryptol* || echo "Strip failed: Ignoring harmless error"
}
install_z3() {
is_exe "$BIN" "z3" && return
case "$RUNNER_OS" in
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"
if $IS_WIN; then 7z x -bd z3.zip; else unzip z3.zip; fi
cp z3-*/bin/z3$EXT $BIN/z3$EXT
$IS_WIN || chmod +x $BIN/z3
rm z3.zip
}
install_cvc4() {
version="${CVC4_VERSION#4.}" # 4.y.z -> y.z
case "$RUNNER_OS" in
Linux) file="x86_64-linux-opt" ;;
Windows) file="win64-opt.exe" ;;
macOS) file="macos-opt" ;;
esac
# Temporary workaround
if [[ "$RUNNER_OS" == "Linux" ]]; then
#latest="$(curl -sSL "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/" | grep linux-opt | tail -n1 | sed -e 's/.*href="//' -e 's/\([^>]*\)">.*$/\1/')"
latest="cvc4-2021-03-13-x86_64-linux-opt"
curl -o cvc4 -sSL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/$latest"
else
curl -o cvc4$EXT -sSL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file"
fi
$IS_WIN || chmod +x cvc4$EXT
mv cvc4$EXT "$BIN/cvc4$EXT"
}
install_yices() {
ext=".tar.gz"
case "$RUNNER_OS" in
Linux) file="pc-linux-gnu-static-gmp.tar.gz" ;;
macOS) file="apple-darwin18.7.0-static-gmp.tar.gz" ;;
Windows) file="pc-mingw32-static-gmp.zip" && ext=".zip" ;;
esac
curl -o "yices$ext" -sL "https://yices.csl.sri.com/releases/$YICES_VERSION/yices-$YICES_VERSION-x86_64-$file"
if $IS_WIN; then
7z x -bd "yices$ext"
mv "yices-$YICES_VERSION"/bin/*.exe "$BIN"
else
tar -xzf "yices$ext"
pushd "yices-$YICES_VERSION" || exit
sudo ./install-yices
popd || exit
fi
rm -rf "yices$ext" "yices-$YICES_VERSION"
}
build() {
ghc_ver="$(ghc --numeric-version)"
cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
@ -114,12 +72,11 @@ build() {
}
install_system_deps() {
install_z3 &
install_cvc4 &
install_yices &
wait
export PATH=$PWD/$BIN:$PATH
echo "$PWD/$BIN" >> "$GITHUB_PATH"
(cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BIN_ZIP_FILE" && unzip -o bins.zip && rm bins.zip)
chmod +x $BIN/*
cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
export PATH=$BIN:$PATH
echo "$BIN" >> "$GITHUB_PATH"
is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
}
@ -165,6 +122,19 @@ zip_dist() {
tar -cvzf "$name".tar.gz "$name"
}
zip_dist_with_solvers() {
: "${VERSION?VERSION is required as an environment variable}"
name="${name:-"cryptol-$VERSION-$RUNNER_OS-x86_64"}"
sname="${name}-with-solvers"
cp "$(which abc)" dist/bin/
cp "$(which cvc4)" dist/bin/
cp "$(which yices)" dist/bin/
cp "$(which yices-smt2)" dist/bin/
cp "$(which z3)" dist/bin/
cp -r dist "$sname"
tar -cvzf "$sname".tar.gz "$sname"
}
output() { echo "::set-output name=$1::$2"; }
ver() { grep Version cryptol.cabal | awk '{print $2}'; }
set_version() { output cryptol-version "$(ver)"; }

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

@ -9,9 +9,7 @@ on:
workflow_dispatch:
env:
Z3_VERSION: "4.8.10"
CVC4_VERSION: "4.1.8"
YICES_VERSION: "2.6.2"
SOLVER_PKG_VERSION: "snapshot-20210917"
jobs:
config:
@ -57,6 +55,8 @@ jobs:
ghc-version: ["8.6.5", "8.8.4", "8.10.2"]
exclude:
# https://gitlab.haskell.org/ghc/ghc/-/issues/18550
- os: windows-latest
ghc-version: 8.8.4
- os: windows-latest
ghc-version: 8.10.2
outputs:
@ -94,6 +94,8 @@ jobs:
- shell: bash
run: .github/ci.sh install_system_deps
env:
BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
- shell: bash
env:
@ -149,19 +151,27 @@ jobs:
SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
run: .github/ci.sh sign cryptol.msi
- if: needs.config.outputs.release == 'true'
shell: bash
env:
SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
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
- shell: bash
run: |
NAME="${{ needs.config.outputs.name }}-${{ runner.os }}-x86_64"
echo "NAME=$NAME" >> $GITHUB_ENV
.github/ci.sh zip_dist_with_solvers $NAME
- if: needs.config.outputs.release == 'true'
shell: bash
env:
SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
run: |
.github/ci.sh sign ${NAME}.tar.gz
.github/ci.sh sign ${NAME}-with-solvers.tar.gz
- uses: actions/upload-artifact@v2
with:
name: ${{ env.NAME }}
@ -169,6 +179,13 @@ jobs:
if-no-files-found: error
retention-days: ${{ needs.config.outputs.retention-days }}
- uses: actions/upload-artifact@v2
with:
name: ${{ env.NAME }}-with-solvers
path: "${{ env.NAME }}-with-solvers.tar.gz*"
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:
@ -197,17 +214,17 @@ jobs:
matrix:
suite: [test-lib]
target: ${{ fromJson(needs.build.outputs.test-lib-json) }}
os: [ubuntu-latest, macos-latest] # , windows-latest]
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: macos-latest
# continue-on-error: false
#- suite: rpc
# target: ''
# os: windows-latest
@ -219,7 +236,7 @@ jobs:
- uses: haskell/actions/setup@v1
with:
ghc-version: '8.10.2'
ghc-version: '8.10.3'
- if: matrix.suite == 'rpc'
uses: actions/setup-python@v2
@ -242,6 +259,8 @@ jobs:
path: bin
- shell: bash
env:
BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
run: |
set -x
chmod +x dist/bin/cryptol
@ -249,6 +268,10 @@ jobs:
chmod +x dist/bin/cryptol-eval-server
chmod +x bin/test-runner
.github/ci.sh install_system_deps
.github/ci.sh deps bin/abc*
.github/ci.sh deps bin/cvc4*
.github/ci.sh deps bin/yices-smt2*
.github/ci.sh deps bin/z3*
ghc_ver="$(ghc --numeric-version)"
cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
cabal v2-update
@ -271,6 +294,7 @@ jobs:
build-push-image:
runs-on: ubuntu-latest
needs: [config]
if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
strategy:
fail-fast: false
matrix:

79
CHANGES.md
View File

@ -1,4 +1,12 @@
# Next Release
# NEXT
## Language changes
* Update the implementation of the Prelude function `sortBy` to use
a merge sort instead of an insertion sort. This improves the both
asymptotic and observed performance on sorting tasks.
# 2.12.0
## Language changes
* Updates to the layout rule. We simplified the specification and made
@ -6,9 +14,76 @@
- Paren blocks nested in a layout block need to respect the indentation
if the layout block
- We allow nested layout blocks to have the same indentation, which is
conveninet when writing `private` declarations as they don't need to
convenient when writing `private` declarations as they don't need to
be indented as long as they are at the end of the file.
* New enumeration forms `[x .. y by n]`, `[x .. <y by n]`,
`[x .. y down by n]` and `[x .. >y down by n]` have been
implemented. These new forms let the user explicitly specify
the stride for an enumeration, as opposed to the previous
`[x, y .. z]` form (where the stride was computed from `x` and `y`).
* Nested modules are now available (from pull request #1048). For example, the following is now valid Cryptol:
module SubmodTest where
import submodule B as C
submodule A where
propA = C::y > 5
submodule B where
y : Integer
y = 42
## New features
* What4 prover backends now feature an improved multi-SAT procedure
which is significantly faster than the old algorithm. Thanks to
Levent Erkök for the suggestion.
* There is a new `w4-abc` solver option, which communicates to ABC
as an external process via What4.
* Expanded support for declaration forms in the REPL. You can now
define infix operators, type synonyms and mutually-recursive functions,
and state signatures and fixity declarations. Multiple declarations
can be combined into a single line by separating them with `;`,
which is necessary for stating a signature together with a
definition, etc.
* There is a new `:set path` REPL option that provides an alternative to
`CRYPTOLPATH` for controlling where to search for imported modules
(issue #631).
* The `cryptol-remote-api` server now natively supports HTTPS (issue
#1008), `newtype` values (issue #1033), and safety checking (issue
#1166).
* Releases optionally include solvers (issue #1111). See the
`*-with-solvers*` files in the assets list for this release.
## Bug fixes
* Closed issues #422, #436, #619, #631, #633, #640, #680, #734, #735,
#759, #760, #764, #849, #996, #1000, #1008, #1019, #1032, #1033,
#1034, #1043, #1047, #1060, #1064, #1083, #1084, #1087, #1102, #1111,
#1113, #1117, #1125, #1133, #1142, #1144, #1145, #1146, #1157, #1160,
#1163, #1166, #1169, #1175, #1179, #1182, #1190, #1191, #1196, #1197,
#1204, #1209, #1210, #1213, #1216, #1223, #1226, #1238, #1239, #1240,
#1241, #1250, #1256, #1259, #1261, #1266, #1274, #1275, #1283, and
#1291.
* Merged pull requests #1048, #1128, #1129, #1130, #1131, #1135, #1136,
#1137, #1139, #1148, #1149, #1150, #1152, #1154, #1156, #1158, #1159,
#1161, #1164, #1165, #1168, #1170, #1171, #1172, #1173, #1174, #1176,
#1181, #1183, #1186, #1188, #1192, #1193, #1194, #1195, #1199, #1200,
#1202, #1203, #1205, #1207, #1211, #1214, #1215, #1218, #1219, #1221,
#1224, #1225, #1227, #1228, #1230, #1231, #1232, #1234, #1242, #1243,
#1244, #1245, #1246, #1247, #1248, #1251, #1252, #1254, #1255, #1258,
#1263, #1265, #1268, #1269, #1270, #1271, #1272, #1273, #1276, #1281,
#1282, #1284, #1285, #1286, #1287, #1288, #1293, #1294, and #1295.
# 2.11.0
## Language changes

86
CODE_OF_CONDUCT.md Normal file
View File

@ -0,0 +1,86 @@
# Code of Conduct
## Our Pledge
We as members, contributors, and leaders pledge to make participation in our
community a harassment-free experience for everyone, regardless of age, body
size, visible or invisible disability, ethnicity, sex characteristics, gender
identity and expression, level of experience, education, socio-economic status,
nationality, personal appearance, race, caste, color, religion, or sexual identity
and orientation.
We pledge to act and interact in ways that contribute to an open, welcoming,
diverse, inclusive, and healthy community.
## Our Standards
Examples of behavior that contributes to a positive environment for our
community include:
* Demonstrating empathy and kindness toward other people
* Being respectful of differing opinions, viewpoints, and experiences
* Giving and gracefully accepting constructive feedback
* Accepting responsibility and apologizing to those affected by our mistakes,
and learning from the experience
* Focusing on what is best not just for us as individuals, but for the
overall community
Examples of unacceptable behavior include:
* The use of sexualized language or imagery, and sexual attention or
advances of any kind
* Trolling, insulting or derogatory comments, and personal or political attacks
* Public or private harassment
* Publishing others' private information, such as a physical or email
address, without their explicit permission
* Other conduct which could reasonably be considered inappropriate in a
professional setting
## Enforcement Responsibilities
Project maintainers are responsible for clarifying and enforcing our standards of
acceptable behavior and will take appropriate and fair corrective action in
response to any behavior that they deem inappropriate, threatening, offensive,
or harmful.
Project maintainers have the right and responsibility to remove, edit, or reject
comments, commits, code, wiki edits, issues, and other contributions that are
not aligned to this Code of Conduct, and will communicate reasons for moderation
decisions when appropriate.
## Scope
This Code of Conduct applies within all community spaces, and also applies when
an individual is officially representing the community in public spaces.
Examples of representing our community include using an official e-mail address,
posting via an official social media account, or acting as an appointed
representative at an online or offline event.
## Enforcement
Instances of abusive, harassing, or otherwise unacceptable behavior may
be reported to the project maintainers responsible for enforcement at
[cryptol@galois.com](mailto:cryptol@galois.com). All complaints will be
reviewed and investigated promptly and fairly.
All project maintainers are obligated to respect the privacy and security of the
reporter of any incident.
## Attribution
This Code of Conduct is adapted from the [Contributor Covenant][homepage],
version 2.1, available at
[https://www.contributor-covenant.org/version/2/1/code_of_conduct.html][v2.1].
Community Impact Guidelines were inspired by
[Mozilla's code of conduct enforcement ladder][Mozilla CoC].
For answers to common questions about this code of conduct, see the FAQ at
[https://www.contributor-covenant.org/faq][FAQ]. Translations are available
at [https://www.contributor-covenant.org/translations][translations].
[homepage]: https://www.contributor-covenant.org
[v2.1]: https://www.contributor-covenant.org/version/2/1/code_of_conduct.html
[Mozilla CoC]: https://github.com/mozilla/diversity
[FAQ]: https://www.contributor-covenant.org/faq
[translations]: https://www.contributor-covenant.org/translations

60
Dockerfile
View File

@ -1,62 +1,21 @@
FROM debian:buster-20210511 AS solvers
# Install needed packages for building
RUN apt-get update \
&& apt-get install -y curl cmake gcc g++ git libreadline-dev unzip
RUN useradd -m user
RUN install -d -o user -g user /solvers
USER user
WORKDIR /solvers
RUN mkdir -p rootfs/usr/local/bin
# Get Z3 4.8.8 from GitHub
RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip --output z3.zip && \
unzip z3.zip && \
mv z3-*/bin/z3 rootfs/usr/local/bin
# Build abc from GitHub. (Latest version.)
RUN git clone https://github.com/berkeley-abc/abc.git && \
( cd abc && make -j$(nproc) ) && \
cp abc/abc rootfs/usr/local/bin
# Build Boolector release 3.2.1 from source
RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz && \
( cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc) ) && \
cp boolector*/build/bin/boolector rootfs/usr/local/bin
# Install Yices 2.6.2
RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz && \
cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
&& cp yices*/bin/yices rootfs/usr/local/bin
# Install CVC4 1.8
# The latest CVC4 1.8 and the release version has a minor discrepency between it, causing sbv to fail
# https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt
#RUN latest="$(curl -sSL 'http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/' | grep linux-opt | tail -n1 | sed -e 's/.*href="//' -e 's/\([^>]*\)">.*$/\1/')" && \
RUN latest="cvc4-2021-03-13-x86_64-linux-opt" && \
curl --output rootfs/usr/local/bin/cvc4 -sSL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/$latest"
# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz
# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin
# Set executable and run tests
RUN chmod +x rootfs/usr/local/bin/*
FROM haskell:8.8.4 AS build
RUN apt-get update && apt-get install -y libncurses-dev
COPY --from=solvers /solvers/rootfs /
RUN apt-get update && apt-get install -y libncurses-dev unzip
RUN useradd -m cryptol
COPY --chown=cryptol:cryptol . /cryptol
USER cryptol
WORKDIR /cryptol
RUN mkdir -p rootfs/usr/local/bin
WORKDIR /cryptol/rootfs/usr/local/bin
RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip"
RUN unzip solvers.zip && rm solvers.zip && chmod +x *
WORKDIR /cryptol
ENV PATH=/cryptol/rootfs/usr/local/bin:$PATH
RUN z3 --version
ARG CRYPTOLPATH="/cryptol/.cryptol"
ENV LANG=C.UTF-8 \
LC_ALL=C.UTF-8
COPY cabal.GHC-8.8.4.config cabal.project.freeze
RUN mkdir -p rootfs/usr/local/bin
RUN cabal v2-update && \
cabal v2-build -j cryptol:exe:cryptol && \
cp $(cabal v2-exec which cryptol) rootfs/usr/local/bin && \
@ -66,8 +25,8 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
RUN ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
# && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
# && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
# && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)
RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
&& cp -r lib/* rootfs/"${CRYPTOLPATH}"
@ -80,7 +39,6 @@ RUN apt-get update \
&& apt-get clean && rm -rf /var/lib/apt/lists/*
RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
COPY --from=build /cryptol/rootfs /
COPY --from=solvers /solvers/rootfs /
USER cryptol
ENV LANG=C.UTF-8 \
LC_ALL=C.UTF-8

6
README.md
View File

@ -46,9 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT
solver](https://github.com/Z3Prover/z3) by default to solve constraints
during type checking, and as the default solver for the `:sat` and
`:prove` commands. Cryptol generally requires the most recent version
of Z3, but you can see the specific version tested in CI by looking for
the `Z3_VERSION` setting in [this
file](https://github.com/GaloisInc/cryptol/blob/master/.github/workflows/ci.yml).
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20210917).
You can download Z3 binaries for a variety of platforms from their
[releases page](https://github.com/Z3Prover/z3/releases). If you
@ -77,7 +75,7 @@ Cryptol builds and runs on various flavors of Linux, Mac OS X, and
Windows. We regularly build and test it in the following environments:
- macOS 10.15, 64-bit
- Ubuntu 18.04, 64-bit
- Ubuntu 20.04, 64-bit
- Windows Server 2019, 64-bit
## Prerequisites

2
cabal.GHC-8.10.2.config
View File

@ -161,7 +161,7 @@ constraints: any.Cabal ==3.2.0.0,
any.semigroups ==0.19.1,
semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers,
any.simple-get-opt ==0.4,
any.simple-smt ==0.9.4,
any.simple-smt ==0.9.7,
any.splitmix ==0.0.5,
splitmix -optimised-mixer +random,
any.statistics ==0.15.2.0,

2
cabal.GHC-8.10.3.config
View File

@ -201,7 +201,7 @@ constraints: any.Cabal ==3.2.1.0,
any.simple-get-opt ==0.4,
any.simple-sendfile ==0.2.30,
simple-sendfile +allow-bsd,
any.simple-smt ==0.9.5,
any.simple-smt ==0.9.7,
any.splitmix ==0.1.0.3,
splitmix -optimised-mixer,
any.statistics ==0.15.2.0,

2
cabal.GHC-8.6.5.config
View File

@ -164,7 +164,7 @@ constraints: any.Cabal ==2.4.0.1,
any.semigroups ==0.19.1,
semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers,
any.simple-get-opt ==0.4,
any.simple-smt ==0.9.4,
any.simple-smt ==0.9.7,
any.splitmix ==0.0.4,
splitmix -optimised-mixer +random,
any.statistics ==0.15.2.0,

2
cabal.GHC-8.8.4.config
View File

@ -161,7 +161,7 @@ constraints: any.Cabal ==3.0.1.0,
any.semigroups ==0.19.1,
semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers,
any.simple-get-opt ==0.4,
any.simple-smt ==0.9.4,
any.simple-smt ==0.9.7,
any.splitmix ==0.0.4,
splitmix -optimised-mixer +random,
any.statistics ==0.15.2.0,

5
cry
View File

@ -23,6 +23,7 @@ Available commands:
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
check-docs Check the exercises embedded in the documentation
EOM
}
@ -97,6 +98,10 @@ case $COMMAND in
$DIR/cryptol-remote-api/check_docs.sh
;;
check-docs)
cabal v2-build exe:check-exercises
find ./docs/ProgrammingCryptol -name '*.tex' -print0 | xargs -0 -n1 cabal v2-exec check-exercises
;;
help) show_usage && exit 0 ;;

8
cryptol-remote-api/CHANGELOG.md
View File

@ -1,5 +1,13 @@
# Revision history for `cryptol-remote-api` and `cryptol-eval-server`
## 2.12.2 -- YYYY-MM-DD
* NEW CHANGELOG ENTRIES SINCE 2.12.0 GO HERE
## 2.12.0 -- 2021-11-19
* v2.12 release
## 2.11.1 -- 2021-06-23
* HTTPS/TLS support added. Enable by running server in `http` mode with `--tls`

51
cryptol-remote-api/Dockerfile
View File

@ -1,59 +1,14 @@
ARG GHCVER="8.10.3"
ARG GHCVER_BOOTSTRAP="8.10.2"
FROM debian:buster-20210511 AS solvers
# Install needed packages for building
RUN apt-get update \
&& apt-get install -y curl cmake gcc g++ git libreadline-dev unzip
RUN useradd -m user
RUN install -d -o user -g user /solvers
USER user
WORKDIR /solvers
RUN mkdir -p rootfs/usr/local/bin
# Get Z3 4.8.8 from GitHub
RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip --output z3.zip && \
unzip z3.zip && \
mv z3-*/bin/z3 rootfs/usr/local/bin
# Build abc from GitHub. (Latest version.)
RUN git clone https://github.com/berkeley-abc/abc.git && \
( cd abc && make -j$(nproc) ) && \
cp abc/abc rootfs/usr/local/bin
# Build Boolector release 3.2.1 from source
RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz && \
( cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc) ) && \
cp boolector*/build/bin/boolector rootfs/usr/local/bin
# Install Yices 2.6.2
RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz && \
cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
&& cp yices*/bin/yices rootfs/usr/local/bin
# Install CVC4 1.8
# The latest CVC4 1.8 and the release version has a minor discrepency between it, causing sbv to fail
# https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt
RUN latest="$(curl -sSL 'http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/' | grep linux-opt | tail -n1 | sed -e 's/.*href="//' -e 's/\([^>]*\)">.*$/\1/')" && \
curl --output rootfs/usr/local/bin/cvc4 -sSL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/$latest"
# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz
# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin
# Set executable and run tests
RUN chmod +x rootfs/usr/local/bin/*
FROM debian:buster-20210511 AS toolchain
ARG PORTABILITY=false
RUN apt-get update && apt-get install -y libncurses-dev libz-dev \
RUN apt-get update && apt-get install -y libncurses-dev libz-dev unzip \
build-essential curl libffi-dev libffi6 libgmp-dev libgmp10 libncurses-dev libncurses5 libtinfo5 libnuma-dev \
$(if ${PORTABILITY}; then echo git autoconf python3; fi)
ENV GHCUP_INSTALL_BASE_PREFIX=/opt \
PATH=/opt/.ghcup/bin:$PATH
RUN curl -o /usr/local/bin/ghcup "https://downloads.haskell.org/~ghcup/0.1.14/x86_64-linux-ghcup-0.1.14" && \
chmod +x /usr/local/bin/ghcup
COPY --from=solvers /solvers/rootfs /
RUN ghcup install cabal --set
ENV PATH=/root/.cabal/bin:$PATH
ADD ./cryptol-remote-api/ghc-portability.patch .
@ -101,6 +56,9 @@ RUN cabal v2-update && \
ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
&& cp -r lib/* rootfs/"${CRYPTOLPATH}"
WORKDIR /cryptol/rootfs/usr/local/bin
RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip" && \
unzip solvers.zip && rm solvers.zip && chmod +x *
USER root
RUN chown -R root:root /cryptol/rootfs
@ -110,7 +68,6 @@ RUN apt-get update \
&& apt-get clean && rm -rf /var/lib/apt/lists/*
RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
COPY --from=build /cryptol/rootfs /
COPY --from=solvers /solvers/rootfs /
USER cryptol
ENV LANG=C.UTF-8 \
LC_ALL=C.UTF-8

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

@ -22,6 +22,8 @@ import CryptolServer.Check ( check, checkDescr )
import CryptolServer.ClearState
( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr)
import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
import CryptolServer.Interrupt
( interruptServer, interruptServerDescr )
import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule)
import Cryptol.TypeCheck.AST (mName)
@ -166,4 +168,8 @@ cryptolEvalMethods =
"clear all states"
clearAllStatesDescr
clearAllStates
, notification
"interrupt"
interruptServerDescr
interruptServer
]

15
cryptol-remote-api/cryptol-remote-api.cabal
View File

@ -1,10 +1,10 @@
cabal-version: 2.4
name: cryptol-remote-api
version: 0.1.0.0
version: 2.12.1
license: BSD-3-Clause
license-file: LICENSE
author: David Thrane Christiansen
maintainer: dtc@galois.com
author: Galois, Inc.
maintainer: cryptol-team@galois.com
category: Language
extra-source-files: CHANGELOG.md
@ -42,7 +42,7 @@ common deps
build-depends:
base >=4.11.1.0 && <4.15,
argo,
aeson >= 1.4.2,
aeson >= 1.4.2 && < 2.1,
base64-bytestring >= 1.0,
bytestring ^>= 0.10.8,
containers >=0.6.0.1 && <0.7,
@ -74,12 +74,16 @@ library
CryptolServer.ExtendSearchPath
CryptolServer.Exceptions
CryptolServer.FocusedModule
CryptolServer.Interrupt
CryptolServer.LoadModule
CryptolServer.Options
CryptolServer.Names
CryptolServer.Sat
CryptolServer.TypeCheck
other-modules:
CryptolServer.AesonCompat
executable cryptol-remote-api
import: deps, warnings, errors
main-is: Main.hs
@ -90,7 +94,8 @@ executable cryptol-remote-api
ghc-options: -threaded -rtsopts -with-rtsopts=-xb0x200000000
build-depends:
cryptol-remote-api, sbv
cryptol-remote-api,
sbv
if os(linux) && flag(static)
ld-options: -static -pthread

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

@ -26,6 +26,8 @@ import CryptolServer.ExtendSearchPath
( extSearchPath, extSearchPathDescr )
import CryptolServer.FocusedModule
( focusedModule, focusedModuleDescr )
import CryptolServer.Interrupt
( interruptServer, interruptServerDescr )
import CryptolServer.LoadModule
( loadFile, loadFileDescr, loadModule, loadModuleDescr )
import CryptolServer.Names ( visibleNames, visibleNamesDescr )
@ -113,4 +115,8 @@ cryptolMethods =
"prove or satisfy"
proveSatDescr
proveSat
, notification
"interrupt"
interruptServerDescr
interruptServer
]

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

@ -557,7 +557,7 @@ Parameter fields
``prover``
The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
@ -611,6 +611,24 @@ Return fields
interrupt (notification)
~~~~~~~~~~~~~~~~~~~~~~~~
Interrupt the server, terminating it's current task (if one exists).
Parameter fields
++++++++++++++++
No parameters
Return fields
+++++++++++++
No return fields

5
cryptol-remote-api/python/.gitignore vendored
View File

@ -128,3 +128,8 @@ dmypy.json
# Pyre type checker
.pyre/
# Files generated from running tests/cryptol/test_cryptol_api.py
*.crt
*.csr
*.key

54
cryptol-remote-api/python/CHANGELOG.md
View File

@ -1,5 +1,59 @@
# Revision history for `cryptol` Python package
## 2.12.4 -- YYYY-MM-DD
* NEW CHANGELOG ENTRIES SINCE 2.12.2 GO HERE
## 2.12.2 -- 2021-12-21
* Add an interface for Cryptol quasiquotation using an f-string-like syntax,
see `tests/cryptol/test_quoting` for some examples.
* Fix a bug with the client's `W4_ABC` solver, add a `W4_ANY` solver.
* Deprecate `CryptolType.from_python` and `CryptolType.convert`
* Remove `CryptolType` arguments to `to_cryptol` and `__to_cryptol__`
## 2.12.0 -- 2021-11-19
* v2.12 release in tandem with Cryptol 2.12 release. See Cryptol release 2.12
release notes for relevant Cryptol changes. No notable changes to RPC server
or client since 2.11.7.
## 2.11.7 -- 2021-09-22
* Add a synchronous, type-annotated interface (`synchronous.py`). To use this
interface, connect using `c = cryptol.sync.connect()` and remove all
`.result()` calls.
* Add a single-connection, synchronous, type-annotated interface based on the
above. To use this interface, add `from cryptol.single_connection import *`,
connect using `connect()`, replace `c.eval(...).result()` with
`cry_eval(...)`, remove all `c.` prefixes, and remove all `.result()` calls.
* Update most of the tests to use the single-connection interface.
## 2.11.6 -- 2021-09-10
* Add a `timeout` field to the `CryptolConnection` class which can be used
to set a default timeout for all RPC interactions.
* Add an optional `timeout` keyword parameter to each `CryptolConnection` method
which can specify a timeout for a particular method call.
* Add an `interrupt` method to the `CryptolConnection` class which interrupts
any active requests on the server.
## 2.11.5 -- 2021-08-25
* From argo: Change the behavior of the `Command` `state` method so that after
a `Command` raises an exception, subsequent interactions will not also raise
the same exception.
## 2.11.4 -- 2021-07-22
* Add client logging option. See the `log_dest` keyword argument on
`cryptol.connect` or the `logging` method on a `CryptolConnection` object.
## 2.11.3 -- 2021-07-20
* Removed automatic reset from `CryptolConnection.__del__`.
## 2.11.2 -- 2021-06-23
* Ability to leverage HTTPS/TLS while _disabling_ verification of SSL certificates.

20
cryptol-remote-api/python/cryptol/__init__.py
View File

@ -16,17 +16,15 @@ from argo_client.connection import DynamicSocketProcess, ServerConnection, Serve
from . import cryptoltypes
from . import solver
from .bitvector import BV
from .cryptoltypes import fail_with
from .quoting import cry, cry_f
from .commands import *
from .connection import *
# import everything from `.synchronous` except `connect` and `connect_stdio`
# (since functions with those names were already imported from `.connection`)
from .synchronous import Qed, Safe, Counterexample, Satisfiable, Unsatisfiable, CryptolSyncConnection
# and add an alias `sync` for the `synchronous` module
from . import synchronous
sync = synchronous
__all__ = ['bitvector', 'commands', 'connections', 'cryptoltypes', 'solver']
def fail_with(x : Exception) -> NoReturn:
"Raise an exception. This is valid in expression positions."
raise x
def cry(string : str) -> cryptoltypes.CryptolCode:
return cryptoltypes.CryptolLiteral(string)
__all__ = ['bitvector', 'commands', 'connection', 'cryptoltypes', 'opaque', 'quoting', 'single_connection', 'solver', 'synchronous']

13
cryptol-remote-api/python/cryptol/bitvector.py
View File

@ -1,8 +1,11 @@
from functools import reduce
from typing import Any, List, Union, Optional, overload
from typing_extensions import Literal
from BitVector import BitVector #type: ignore
ByteOrder = Union[Literal['little'], Literal['big']]
class BV:
"""A class representing a cryptol bit vector (i.e., a sequence of bits).
@ -211,7 +214,7 @@ class BV:
return bin(self).count("1")
@staticmethod
def from_bytes(bs : bytes, *, size : Optional[int] =None, byteorder : str ='big') -> 'BV':
def from_bytes(bs : Union[bytes,bytearray], *, size : Optional[int] = None, byteorder : ByteOrder = 'big') -> 'BV':
"""Convert the given bytes ``bs`` into a ``BV``.
:param bs: Bytes to convert to a ``BV``.
@ -221,11 +224,13 @@ class BV:
``'big'``, ``little`` being the other acceptable value. Equivalent to the ``byteorder``
parameter from Python's ``int.from_bytes``."""
if not isinstance(bs, bytes):
raise ValueError("from_bytes given not bytes value: {bs!r}")
if isinstance(bs, bytearray):
bs = bytes(bs)
elif not isinstance(bs, bytes):
raise ValueError(f"from_bytes given not a bytearray or bytes value: {bs!r}")
if not byteorder == 'little' and not byteorder == 'big':
raise ValueError("from_bytes given not bytes value: {bs!r}")
raise ValueError("byteorder must be either 'little' or 'big'")
if size == None:
return BV(len(bs) * 8, int.from_bytes(bs, byteorder=byteorder))

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

@ -2,9 +2,10 @@
from __future__ import annotations
import base64
from abc import ABC
from enum import Enum
from dataclasses import dataclass
from typing import Any, List, Optional, Union
from typing import Any, Tuple, List, Dict, Optional, Union
from typing_extensions import Literal
import argo_client.interaction as argo
@ -20,7 +21,9 @@ def extend_hex(string : str) -> str:
else:
return string
def from_cryptol_arg(val : Any) -> Any:
CryptolValue = Union[bool, int, BV, Tuple, List, Dict, OpaqueValue]
def from_cryptol_arg(val : Any) -> CryptolValue:
"""Return the canonical Python value for a Cryptol JSON value."""
if isinstance(val, bool):
return val
@ -33,7 +36,7 @@ def from_cryptol_arg(val : Any) -> Any:
elif tag == 'tuple':
return tuple(from_cryptol_arg(x) for x in val['data'])
elif tag == 'record':
return {k : from_cryptol_arg(val[k]) for k in val['data']}
return {k : from_cryptol_arg(val['data'][k]) for k in val['data']}
elif tag == 'sequence':
return [from_cryptol_arg(v) for v in val['data']]
elif tag == 'bits':
@ -59,48 +62,59 @@ def from_cryptol_arg(val : Any) -> Any:
class CryptolLoadModule(argo.Command):
def __init__(self, connection : HasProtocolState, mod_name : str) -> None:
super(CryptolLoadModule, self).__init__('load module', {'module name': mod_name}, connection)
def __init__(self, connection : HasProtocolState, mod_name : str, timeout: Optional[float]) -> None:
super(CryptolLoadModule, self).__init__('load module', {'module name': mod_name}, connection, timeout=timeout)
def process_result(self, res : Any) -> Any:
return res
class CryptolLoadFile(argo.Command):
def __init__(self, connection : HasProtocolState, filename : str) -> None:
super(CryptolLoadFile, self).__init__('load file', {'file': filename}, connection)
def __init__(self, connection : HasProtocolState, filename : str, timeout: Optional[float]) -> None:
super(CryptolLoadFile, self).__init__('load file', {'file': filename}, connection, timeout=timeout)
def process_result(self, res : Any) -> Any:
return res
class CryptolExtendSearchPath(argo.Command):
def __init__(self, connection : HasProtocolState, dirs : List[str]) -> None:
super(CryptolExtendSearchPath, self).__init__('extend search path', {'paths': dirs}, connection)
def __init__(self, connection : HasProtocolState, dirs : List[str], timeout: Optional[float]) -> None:
super(CryptolExtendSearchPath, self).__init__('extend search path', {'paths': dirs}, connection, timeout=timeout)
def process_result(self, res : Any) -> Any:
return res
class CryptolEvalExpr(argo.Command):
def __init__(self, connection : HasProtocolState, expr : Any) -> None:
super(CryptolEvalExpr, self).__init__(
class CryptolEvalExprRaw(argo.Command):
def __init__(self, connection : HasProtocolState, expr : Any, timeout: Optional[float]) -> None:
super(CryptolEvalExprRaw, self).__init__(
'evaluate expression',
{'expression': expr},
connection
connection,
timeout=timeout
)
def process_result(self, res : Any) -> Any:
return from_cryptol_arg(res['value'])
return res['value']
class CryptolCall(argo.Command):
def __init__(self, connection : HasProtocolState, fun : str, args : List[Any]) -> None:
super(CryptolCall, self).__init__(
class CryptolEvalExpr(CryptolEvalExprRaw):
def process_result(self, res : Any) -> Any:
return from_cryptol_arg(super(CryptolEvalExpr, self).process_result(res))
class CryptolCallRaw(argo.Command):
def __init__(self, connection : HasProtocolState, fun : str, args : List[Any], timeout: Optional[float]) -> None:
super(CryptolCallRaw, self).__init__(
'call',
{'function': fun, 'arguments': args},
connection
connection,
timeout=timeout
)
def process_result(self, res : Any) -> Any:
return from_cryptol_arg(res['value'])
return res['value']
class CryptolCall(CryptolCallRaw):
def process_result(self, res : Any) -> Any:
return from_cryptol_arg(super(CryptolCall, self).process_result(res))
@dataclass
@ -111,75 +125,103 @@ class CheckReport:
error_msg: Optional[str]
tests_run: int
tests_possible: Optional[int]
def __bool__(self) -> bool:
return self.success
class CryptolCheck(argo.Command):
def __init__(self, connection : HasProtocolState, expr : Any, num_tests : Union[Literal['all'],int, None]) -> None:
def to_check_report(res : Any) -> CheckReport:
if res['result'] == 'pass':
return CheckReport(
success=True,
args=[],
error_msg = None,
tests_run=res['tests run'],
tests_possible=res['tests possible'])
elif res['result'] == 'fail':
return CheckReport(
success=False,
args=[from_cryptol_arg(arg['expr']) for arg in res['arguments']],
error_msg = None,
tests_run=res['tests run'],
tests_possible=res['tests possible'])
elif res['result'] == 'error':
return CheckReport(
success=False,
args=[from_cryptol_arg(arg['expr']) for arg in res['arguments']],
error_msg = res['error message'],
tests_run=res['tests run'],
tests_possible=res['tests possible'])
else:
raise ValueError("Unknown check result " + str(res))
class CryptolCheckRaw(argo.Command):
def __init__(self, connection : HasProtocolState,
expr : Any,
num_tests : Union[Literal['all'],int, None],
timeout: Optional[float]) -> None:
if num_tests:
args = {'expression': expr, 'number of tests':num_tests}
else:
args = {'expression': expr}
super(CryptolCheck, self).__init__(
super(CryptolCheckRaw, self).__init__(
'check',
args,
connection
connection,
timeout=timeout
)
def process_result(self, res : Any) -> Any:
return res
class CryptolCheck(CryptolCheckRaw):
def process_result(self, res : Any) -> 'CheckReport':
if res['result'] == 'pass':
return CheckReport(
success=True,
args=[],
error_msg = None,
tests_run=res['tests run'],
tests_possible=res['tests possible'])
elif res['result'] == 'fail':
return CheckReport(
success=False,
args=[from_cryptol_arg(arg['expr']) for arg in res['arguments']],
error_msg = None,
tests_run=res['tests run'],
tests_possible=res['tests possible'])
elif res['result'] == 'error':
return CheckReport(
success=False,
args=[from_cryptol_arg(arg['expr']) for arg in res['arguments']],
error_msg = res['error message'],
tests_run=res['tests run'],
tests_possible=res['tests possible'])
else:
raise ValueError("Unknown check result " + str(res))
return to_check_report(super(CryptolCheck, self).process_result(res))
class CryptolCheckType(argo.Command):
def __init__(self, connection : HasProtocolState, expr : Any) -> None:
def __init__(self, connection : HasProtocolState, expr : Any, timeout: Optional[float]) -> None:
super(CryptolCheckType, self).__init__(
'check type',
{'expression': expr},
connection
connection,
timeout=timeout
)
def process_result(self, res : Any) -> Any:
return res['type schema']
class SmtQueryType(str, Enum):
PROVE = 'prove'
SAFE = 'safe'
SAT = 'sat'
class CryptolProveSat(argo.Command):
def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : Solver, count : Optional[int]) -> None:
super(CryptolProveSat, self).__init__(
class CryptolProveSatRaw(argo.Command):
def __init__(self,
connection : HasProtocolState,
qtype : SmtQueryType,
expr : Any,
solver : Solver,
count : Optional[int],
timeout: Optional[float]) -> None:
super(CryptolProveSatRaw, self).__init__(
'prove or satisfy',
{'query type': qtype,
'expression': expr,
'prover': solver.name(),
'hash consing': "true" if solver.hash_consing() else "false",
'result count': 'all' if count is None else count},
connection
connection,
timeout=timeout
)
self.qtype = qtype
def process_result(self, res : Any) -> Any:
return res
class CryptolProveSat(CryptolProveSatRaw):
def process_result(self, res : Any) -> Any:
res = super(CryptolProveSat, self).process_result(res)
if res['result'] == 'unsatisfiable':
if self.qtype == SmtQueryType.SAT:
return False
@ -199,36 +241,49 @@ class CryptolProveSat(argo.Command):
else:
raise ValueError("Unknown SMT result: " + str(res))
class CryptolProveRaw(CryptolProveSatRaw):
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
super(CryptolProveRaw, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1, timeout)
class CryptolProve(CryptolProveSat):
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1)
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1, timeout=timeout)
class CryptolSatRaw(CryptolProveSatRaw):
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int, timeout: Optional[float]) -> None:
super(CryptolSatRaw, self).__init__(connection, SmtQueryType.SAT, expr, solver, count, timeout=timeout)
class CryptolSat(CryptolProveSat):
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int) -> None:
super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count)
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int, timeout: Optional[float]) -> None:
super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count, timeout=timeout)
class CryptolSafeRaw(CryptolProveSatRaw):
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
super(CryptolSafeRaw, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1, timeout=timeout)
class CryptolSafe(CryptolProveSat):
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1)
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, timeout: Optional[float]) -> None:
super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1, timeout=timeout)
class CryptolNames(argo.Command):
def __init__(self, connection : HasProtocolState) -> None:
super(CryptolNames, self).__init__('visible names', {}, connection)
def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None:
super(CryptolNames, self).__init__('visible names', {}, connection, timeout=timeout)
def process_result(self, res : Any) -> Any:
return res
class CryptolFocusedModule(argo.Command):
def __init__(self, connection : HasProtocolState) -> None:
def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None:
super(CryptolFocusedModule, self).__init__(
'focused module',
{},
connection
connection,
timeout=timeout
)
def process_result(self, res : Any) -> Any:
return res
class CryptolReset(argo.Notification):
def __init__(self, connection : HasProtocolState) -> None:
super(CryptolReset, self).__init__(
@ -237,6 +292,7 @@ class CryptolReset(argo.Notification):
connection
)
class CryptolResetServer(argo.Notification):
def __init__(self, connection : HasProtocolState) -> None:
super(CryptolResetServer, self).__init__(
@ -244,3 +300,11 @@ class CryptolResetServer(argo.Notification):
{},
connection
)
class CryptolInterrupt(argo.Notification):
def __init__(self, connection : HasProtocolState) -> None:
super(CryptolInterrupt, self).__init__(
'interrupt',
{},
connection
)

268
cryptol-remote-api/python/cryptol/connection.py
View File

@ -2,15 +2,18 @@
from __future__ import annotations
import os
import sys
from distutils.spawn import find_executable
from typing import Any, List, Optional, Union
from typing import Any, List, Optional, Union, TextIO
from typing_extensions import Literal
import argo_client.interaction as argo
from argo_client.connection import DynamicSocketProcess, ServerConnection, ServerProcess, StdIOProcess, HttpProcess
from .custom_fstring import *
from .quoting import *
from . import cryptoltypes
from . import solver
from .commands import *
from .commands import *
def connect(command : Optional[str]=None,
@ -18,7 +21,9 @@ def connect(command : Optional[str]=None,
cryptol_path : Optional[str] = None,
url : Optional[str] = None,
reset_server : bool = False,
verify : Union[bool, str] = True) -> CryptolConnection:
verify : Union[bool, str] = True,
log_dest : Optional[TextIO] = None,
timeout : Optional[float] = None) -> CryptolConnection:
"""
Connect to a (possibly new) Cryptol server process.
@ -39,6 +44,14 @@ def connect(command : Optional[str]=None,
only has an affect when ``connect`` is called with a ``url`` parameter
or when the ``CRYPTOL_SERVER_URL`` environment variable is set.
:param log_dest: A destination to log JSON requests/responses to, e.g. ``log_dest=sys.stderr``
will print traffic to ``stderr``, ``log_dest=open('foo.log', 'w')`` will log to ``foo.log``,
etc.
:param timeout: Optional default timeout (in seconds) for methods. Can be modified/read via the
`timeout` member field on a `CryptolConnection` or the `get_default_timeout` and
`set_default_timeout` methods. Method invocations which specify the optional `timeout` keyword
parameter will cause the default to be ignored for that method.
If no ``command`` or ``url`` parameters are provided, the following are attempted in order:
@ -56,27 +69,27 @@ def connect(command : Optional[str]=None,
if command is not None:
if url is not None:
raise ValueError("A Cryptol server URL cannot be specified with a command currently.")
c = CryptolConnection(command, cryptol_path)
c = CryptolConnection(command, cryptol_path, log_dest=log_dest, timeout=timeout)
# User-passed url?
if c is None and url is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url, verify=verify)), cryptol_path)
c = CryptolConnection(ServerConnection(HttpProcess(url, verify=verify)), cryptol_path, log_dest=log_dest)
# Check `CRYPTOL_SERVER` env var if no connection identified yet
if c is None:
command = os.getenv('CRYPTOL_SERVER')
if command is not None:
command = find_executable(command)
if command is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path, log_dest=log_dest, timeout=timeout)
# Check `CRYPTOL_SERVER_URL` env var if no connection identified yet
if c is None:
url = os.getenv('CRYPTOL_SERVER_URL')
if url is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url,verify=verify)), cryptol_path)
c = CryptolConnection(ServerConnection(HttpProcess(url,verify=verify)), cryptol_path, log_dest=log_dest, timeout=timeout)
# Check if `cryptol-remote-api` is in the PATH if no connection identified yet
if c is None:
command = find_executable('cryptol-remote-api')
if command is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path, log_dest=log_dest, timeout=timeout)
# Raise an error if still no connection identified yet
if c is not None:
if reset_server:
@ -92,7 +105,10 @@ def connect(command : Optional[str]=None,
def connect_stdio(command : str, cryptol_path : Optional[str] = None) -> CryptolConnection:
def connect_stdio(command : str,
cryptol_path : Optional[str] = None,
log_dest : Optional[TextIO] = None,
timeout : Optional[float] = None) -> CryptolConnection:
"""Start a new connection to a new Cryptol server process.
:param command: The command to launch the Cryptol server.
@ -100,10 +116,19 @@ def connect_stdio(command : str, cryptol_path : Optional[str] = None) -> Cryptol
:param cryptol_path: An optional replacement for the contents of
the ``CRYPTOLPATH`` environment variable.
:param log_dest: A destination to log JSON requests/responses to, e.g. ``log_dest=sys.stderr``
will print traffic to ``stderr``, ``log_dest=open('foo.log', 'w')`` will log to ``foo.log``,
etc.
:param timeout: Optional default timeout (in seconds) for methods. Can be modified/read via the
`timeout` member field on a `CryptolConnection` or the `get_default_timeout` and
`set_default_timeout` methods. Method invocations which specify the optional `timeout` keyword
parameter will cause the default to be ignored for that method.
"""
conn = CryptolStdIOProcess(command, cryptol_path=cryptol_path)
return CryptolConnection(conn)
return CryptolConnection(conn, log_dest=log_dest, timeout=timeout)
class CryptolConnection:
@ -120,21 +145,36 @@ class CryptolConnection:
sequential state dependencies between commands.
"""
most_recent_result : Optional[argo.Interaction]
proc: ServerProcess
timeout : Optional[float]
"""(Optional) default timeout in seconds for methods."""
def __init__(self,
command_or_connection : Union[str, ServerConnection, ServerProcess],
cryptol_path : Optional[str] = None) -> None:
cryptol_path : Optional[str] = None,
*,
log_dest : Optional[TextIO] = None,
timeout : Optional[float] = None) -> None:
self.most_recent_result = None
self.timeout = timeout
if isinstance(command_or_connection, ServerProcess):
self.proc = command_or_connection
self.server_connection = ServerConnection(self.proc)
self.server_connection = ServerConnection(command_or_connection)
elif isinstance(command_or_connection, str):
self.proc = CryptolDynamicSocketProcess(command_or_connection, cryptol_path=cryptol_path)
self.server_connection = ServerConnection(self.proc)
self.server_connection = ServerConnection(CryptolDynamicSocketProcess(command_or_connection, cryptol_path=cryptol_path))
else:
self.server_connection = command_or_connection
if log_dest:
self.logging(on=True,dest=log_dest)
def get_default_timeout(self) -> Optional[float]:
"""Get the value of the optional default timeout for methods (in seconds)."""
return self.timeout
def set_default_timeout(self, timeout : Optional[float]) -> None:
"""Set the value of the optional default timeout for methods (in seconds)."""
self.timeout = timeout
# Currently disabled in (overly?) conservative effort to not accidentally
# duplicate and share mutable state.
@ -154,96 +194,204 @@ class CryptolConnection:
return self.most_recent_result.state()
# Protocol messages
def load_file(self, filename : str) -> argo.Command:
def load_file(self, filename : str, *, timeout:Optional[float] = None) -> argo.Command:
"""Load a filename as a Cryptol module, like ``:load`` at the Cryptol
REPL.
:param timeout: Optional timeout for this request (in seconds).
"""
self.most_recent_result = CryptolLoadFile(self, filename)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolLoadFile(self, filename, timeout)
return self.most_recent_result
def load_module(self, module_name : str) -> argo.Command:
"""Load a Cryptol module, like ``:module`` at the Cryptol REPL."""
self.most_recent_result = CryptolLoadModule(self, module_name)
return self.most_recent_result
def load_module(self, module_name : str, *, timeout:Optional[float] = None) -> argo.Command:
"""Load a Cryptol module, like ``:module`` at the Cryptol REPL.
def eval(self, expression : Any) -> argo.Command:
"""Evaluate a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing
for their JSON equivalents.
:param timeout: Optional timeout for this request (in seconds).
"""
self.most_recent_result = CryptolEvalExpr(self, expression)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolLoadModule(self, module_name, timeout)
return self.most_recent_result
def evaluate_expression(self, expression : Any) -> argo.Command:
def eval_raw(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
"""Like the member method ``eval``, but does not call
``from_cryptol_arg`` on the ``.result()``.
:param timeout: Optional timeout for this request (in seconds).
"""
if hasattr(expression, '__to_cryptol__'):
expression = cryptoltypes.to_cryptol(expression)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolEvalExprRaw(self, expression, timeout)
return self.most_recent_result
def eval(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
"""Evaluate a Cryptol expression, with the result represented
according to :ref:`cryptol-json-expression`, with Python datatypes
standing for their JSON equivalents.
:param timeout: Optional timeout for this request (in seconds).
"""
if hasattr(expression, '__to_cryptol__'):
expression = cryptoltypes.to_cryptol(expression)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolEvalExpr(self, expression, timeout)
return self.most_recent_result
def eval_f(self, s : str, *, timeout:Optional[float] = None) -> argo.Command:
"""Parses the given string like ``cry_f``, then evalues it, with the
result represented according to :ref:`cryptol-json-expression`, with
Python datatypes standing for their JSON equivalents.
:param timeout: Optional timeout for this request (in seconds).
"""
expression = to_cryptol_str_customf(s, frames=1, filename="<eval_f>")
return self.eval(expression, timeout=timeout)
def evaluate_expression(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
"""Synonym for member method ``eval``.
:param timeout: Optional timeout for this request (in seconds)."""
return self.eval(expression, timeout=timeout)
def extend_search_path(self, *dir : str, timeout:Optional[float] = None) -> argo.Command:
"""Extend the search path for loading Cryptol modules.
:param timeout: Optional timeout for this request (in seconds)."""
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolExtendSearchPath(self, list(dir), timeout)
return self.most_recent_result
def call_raw(self, fun : str, *args : List[Any], timeout:Optional[float] = None) -> argo.Command:
"""Like the member method ``call``, but does not call
``from_cryptol_arg`` on the ``.result()``.
"""
return self.eval(expression)
def extend_search_path(self, *dir : str) -> argo.Command:
"""Load a Cryptol module, like ``:module`` at the Cryptol REPL."""
self.most_recent_result = CryptolExtendSearchPath(self, list(dir))
timeout = timeout if timeout is not None else self.timeout
encoded_args = [cryptoltypes.to_cryptol(a) for a in args]
self.most_recent_result = CryptolCallRaw(self, fun, encoded_args, timeout)
return self.most_recent_result
def call(self, fun : str, *args : List[Any]) -> argo.Command:
encoded_args = [cryptoltypes.CryptolType().from_python(a) for a in args]
self.most_recent_result = CryptolCall(self, fun, encoded_args)
def call(self, fun : str, *args : List[Any], timeout:Optional[float] = None) -> argo.Command:
"""Call function ``fun`` with specified ``args``.
:param timeout: Optional timeout for this request (in seconds)."""
timeout = timeout if timeout is not None else self.timeout
encoded_args = [cryptoltypes.to_cryptol(a) for a in args]
self.most_recent_result = CryptolCall(self, fun, encoded_args, timeout)
return self.most_recent_result
def check(self, expr : Any, *, num_tests : Union[Literal['all'], int, None] = None) -> argo.Command:
def check_raw(self, expr : Any, *, num_tests : Union[Literal['all'], int, None] = None, timeout:Optional[float] = None) -> argo.Command:
"""Like the member method ``check``, but does not call
`to_check_report` on the ``.result()``.
"""
timeout = timeout if timeout is not None else self.timeout
if num_tests == "all" or isinstance(num_tests, int) or num_tests is None:
self.most_recent_result = CryptolCheckRaw(self, expr, num_tests, timeout)
return self.most_recent_result
else:
raise ValueError('``num_tests`` must be an integer, ``None``, or the string literall ``"all"``')
def check(self, expr : Any, *, num_tests : Union[Literal['all'], int, None] = None, timeout:Optional[float] = None) -> argo.Command:
"""Tests the validity of a Cryptol expression with random inputs. The expression must be a function with
return type ``Bit``.
If ``num_tests`` is ``"all"`` then the expression is tested exhaustively (i.e., against all possible inputs).
If ``num_tests`` is omitted, Cryptol defaults to running 100 tests.
:param timeout: Optional timeout for this request (in seconds).
"""
timeout = timeout if timeout is not None else self.timeout
if num_tests == "all" or isinstance(num_tests, int) or num_tests is None:
self.most_recent_result = CryptolCheck(self, expr, num_tests)
self.most_recent_result = CryptolCheck(self, expr, num_tests, timeout)
return self.most_recent_result
else:
raise ValueError('``num_tests`` must be an integer, ``None``, or the string literall ``"all"``')
def check_type(self, code : Any) -> argo.Command:
def check_type(self, code : Any, *, timeout:Optional[float] = None) -> argo.Command:
"""Check the type of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents.
:param timeout: Optional timeout for this request (in seconds).
"""
self.most_recent_result = CryptolCheckType(self, code)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolCheckType(self, code, timeout)
return self.most_recent_result
def sat(self, expr : Any, solver : solver.Solver = solver.Z3, count : int = 1) -> argo.Command:
def sat_raw(self, expr : Any, solver : solver.Solver = solver.Z3, count : int = 1, *, timeout:Optional[float] = None) -> argo.Command:
"""Like the member method ``sat``, but does not call
`to_smt_query_result` on the ``.result()``.
"""
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolSatRaw(self, expr, solver, count, timeout)
return self.most_recent_result
def sat(self, expr : Any, solver : solver.Solver = solver.Z3, count : int = 1, *, timeout:Optional[float] = None) -> argo.Command:
"""Check the satisfiability of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`, and return up to
`count` solutions.
:param timeout: Optional timeout for this request (in seconds).
"""
self.most_recent_result = CryptolSat(self, expr, solver, count)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolSat(self, expr, solver, count, timeout)
return self.most_recent_result
def prove(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Command:
def prove_raw(self, expr : Any, solver : solver.Solver = solver.Z3, *, timeout:Optional[float] = None) -> argo.Command:
"""Like the member method ``prove``, but does not call
`to_smt_query_result` on the ``.result()``.
"""
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolProveRaw(self, expr, solver, timeout)
return self.most_recent_result
def prove(self, expr : Any, solver : solver.Solver = solver.Z3, *, timeout:Optional[float] = None) -> argo.Command:
"""Check the validity of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`.
:param timeout: Optional timeout for this request (in seconds).
"""
self.most_recent_result = CryptolProve(self, expr, solver)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolProve(self, expr, solver, timeout)
return self.most_recent_result
def safe(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Command:
def safe_raw(self, expr : Any, solver : solver.Solver = solver.Z3, *, timeout:Optional[float] = None) -> argo.Command:
"""Like the member method ``safe``, but does not call
`to_smt_query_result` on the ``.result()``.
"""
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolSafeRaw(self, expr, solver, timeout)
return self.most_recent_result
def safe(self, expr : Any, solver : solver.Solver = solver.Z3, *, timeout:Optional[float] = None) -> argo.Command:
"""Check via an external SMT solver that the given term is safe for all inputs,
which means it cannot encounter a run-time error.
:param timeout: Optional timeout for this request (in seconds).
"""
self.most_recent_result = CryptolSafe(self, expr, solver)
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolSafe(self, expr, solver, timeout)
return self.most_recent_result
def names(self) -> argo.Command:
"""Discover the list of names currently in scope in the current context."""
self.most_recent_result = CryptolNames(self)
def names(self, *, timeout:Optional[float] = None) -> argo.Command:
"""Discover the list of names currently in scope in the current context.
:param timeout: Optional timeout for this request (in seconds)."""
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolNames(self, timeout)
return self.most_recent_result
def focused_module(self) -> argo.Command:
"""Return the name of the currently-focused module."""
self.most_recent_result = CryptolFocusedModule(self)
def focused_module(self, *, timeout:Optional[float] = None) -> argo.Command:
"""Return the name of the currently-focused module.
:param timeout: Optional timeout for this request (in seconds)."""
timeout = timeout if timeout is not None else self.timeout
self.most_recent_result = CryptolFocusedModule(self, timeout)
return self.most_recent_result
def reset(self) -> None:
@ -258,13 +406,13 @@ class CryptolConnection:
CryptolResetServer(self)
self.most_recent_result = None
def __del__(self) -> None:
# when being deleted, ensure we don't have a lingering state on the server
if self.most_recent_result is not None:
try:
CryptolReset(self)
except Exception:
pass
def interrupt(self) -> None:
"""Interrupt the Cryptol server, cancelling any in-progress requests."""
CryptolInterrupt(self)
def logging(self, on : bool, *, dest : TextIO = sys.stderr) -> None:
"""Whether to log received and transmitted JSON."""
self.server_connection.logging(on=on,dest=dest)
class CryptolDynamicSocketProcess(DynamicSocketProcess):
@ -321,7 +469,7 @@ class CryptolStdIOProcess(StdIOProcess):
# current_expr = self.name
# found_args = []
# while len(arg_types) > 0 and len(remaining_args) > 0:
# found_args.append(arg_types[0].from_python(remaining_args[0]))
# found_args.append(to_cryptol(remaining_args[0]))
# current_expr = {'expression': 'call', 'function': self.name, 'arguments': found_args}
# ty = self.connection.check_type(current_expr).result()
# current_type = cryptoltypes.to_schema(ty)

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

@ -1,103 +1,178 @@
from __future__ import annotations
from collections import OrderedDict
from abc import ABCMeta, abstractmethod
from dataclasses import dataclass
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
from typing_extensions import Literal, Protocol
import typing
from typing import cast, Any, Dict, Iterable, List, NoReturn, Optional, TypeVar, Union
import typing_extensions
from typing_extensions import Protocol, runtime_checkable
A = TypeVar('A')
# -----------------------------------------------------------
# CryptolJSON and CryptolCode
# -----------------------------------------------------------
def is_parenthesized(s : str) -> bool:
"""Returns ``True`` iff the given string has balanced parentheses and is
enclosed in a matching pair of parentheses.
:examples:
>>> is_parenthesized(' ((a) b )')
True
>>> is_parenthesized('(a) (b)')
False
>>> is_parenthesized('(a')
False
"""
seen_one, depth = False, 0
for c in s:
if depth > 0:
if c == '(': depth += 1
if c == ')': depth -= 1
else: # depth == 0
if c == '(':
if not seen_one: seen_one, depth = True, 1
# A new left paren after all parens have been closed means our
# string is not enclosed in a matching pair of parentheses
else: return False
if c == ')':
# A right paren with no matching left means our string does
# not have balanced parentheses
return False
# Return True if in the end all parentheses are balanced and we've seen at
# least one matching pair
return seen_one and depth == 0
def parenthesize(s : str) -> str:
"""Encloses the given string ``s`` in parentheses if
``is_parenthesized(s)`` is ``False``"""
return s if is_parenthesized(s) else f'({s})'
JSON = Union[bool, int, float, str, Dict, typing.Tuple, List]
@runtime_checkable
class CryptolJSON(Protocol):
def __to_cryptol__(self, ty : CryptolType) -> Any: ...
"""A ``Protocol`` for objects which can be converted to Cryptol JSON or
Cryptol strings."""
def __to_cryptol__(self) -> JSON: ...
def __to_cryptol_str__(self) -> str: ...
class CryptolCode(metaclass=ABCMeta):
def __call__(self, other : CryptolJSON) -> CryptolCode:
return CryptolApplication(self, other)
"""The base class for ``CryptolLiteral`` and ``CryptolApplication``."""
@abstractmethod
def __to_cryptol__(self, ty : CryptolType) -> Any: ...
def __to_cryptol__(self) -> JSON: ...
@abstractmethod
def __to_cryptol_str__(self) -> str: ...
def __str__(self) -> str:
return self.__to_cryptol_str__()
def __call__(self, *others : CryptolJSON) -> CryptolCode:
return CryptolApplication(self, *others)
@dataclass
class CryptolLiteral(CryptolCode):
def __init__(self, code : str) -> None:
self._code = code
"""A string of Cryptol syntax."""
_code : str
def __to_cryptol__(self, ty : CryptolType) -> Any:
def __to_cryptol__(self) -> JSON:
return self._code
def __to_cryptol_str__(self) -> str:
return self._code
@dataclass
class CryptolApplication(CryptolCode):
def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None:
self._rator = rator
self._rands = rands
"""An application of a Cryptol function to some arguments."""
_rator : CryptolJSON
_rands : typing.Sequence[CryptolJSON]
def __to_cryptol__(self, ty : CryptolType) -> Any:
def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None:
if all(isinstance(rand, CryptolJSON) for rand in rands):
self._rator = rator
self._rands = rands
else:
args_str = ", ".join(map(repr, [rator, *rands]))
raise ValueError("Arguments given to CryptolApplication must be CryptolJSON: " + args_str)
def __repr__(self) -> str:
return f'CryptolApplication({", ".join(repr(x) for x in [self._rator, *self._rands])})'
def __to_cryptol__(self) -> JSON:
return {'expression': 'call',
'function': to_cryptol(self._rator),
'arguments': [to_cryptol(arg) for arg in self._rands]}
class CryptolArrowKind:
def __init__(self, dom : CryptolKind, ran : CryptolKind):
self.domain = dom
self.range = ran
def __to_cryptol_str__(self) -> str:
if len(self._rands) == 0:
return self._rator.__to_cryptol_str__()
else:
return ' '.join(parenthesize(x.__to_cryptol_str__()) for x in [self._rator, *self._rands])
def __repr__(self) -> str:
return f"CryptolArrowKind({self.domain!r}, {self.range!r})"
CryptolKind = Union[Literal['Type'], Literal['Num'], Literal['Prop'], CryptolArrowKind]
# -----------------------------------------------------------
# Converting Python terms to Cryptol JSON
# -----------------------------------------------------------
def to_kind(k : Any) -> CryptolKind:
if k == "Type": return "Type"
elif k == "Num": return "Num"
elif k == "Prop": return "Prop"
elif k['kind'] == "arrow":
return CryptolArrowKind(k['from'], k['to'])
def to_cryptol(val : Any) -> JSON:
"""Convert a ``CryptolJSON`` value, a Python value representing a Cryptol
term, or any combination of the two to Cryptol JSON."""
if isinstance(val, bool):
return val
elif isinstance(val, tuple) and val == ():
return {'expression': 'unit'}
elif isinstance(val, tuple):
return {'expression': 'tuple',
'data': [to_cryptol(x) for x in val]}
elif isinstance(val, dict):
return {'expression': 'record',
'data': {k : to_cryptol(val[k])
if isinstance(k, str)
else fail_with (TypeError("Record keys must be strings"))
for k in val}}
elif isinstance(val, int):
return val
elif isinstance(val, list):
return {'expression': 'sequence',
'data': [to_cryptol(v) for v in val]}
elif isinstance(val, bytes) or isinstance(val, bytearray):
return {'expression': 'bits',
'encoding': 'base64',
'width': 8 * len(val),
'data': base64.b64encode(val).decode('ascii')}
elif isinstance(val, BitVector.BitVector):
n = int(val)
byte_width = ceil(n.bit_length()/8)
return {'expression': 'bits',
'encoding': 'base64',
'width': val.length(), # N.B. original length, not padded
'data': base64.b64encode(n.to_bytes(byte_width,'big')).decode('ascii')}
elif isinstance(val, BV):
return {'expression': 'bits',
'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}
elif hasattr(val, '__to_cryptol__'):
code = val.__to_cryptol__()
if is_plausible_json(code):
# the call to is_plausible_json ensures this cast is OK
return cast(JSON, code)
else:
raise ValueError(f"Improbable JSON from __to_cryptol__: {val!r} gave {code!r}")
else:
raise ValueError(f'Not a Cryptol kind: {k!r}')
class CryptolProp:
pass
class UnaryProp(CryptolProp):
def __init__(self, subject : CryptolType) -> None:
self.subject = subject
class Fin(UnaryProp):
def __repr__(self) -> str:
return f"Fin({self.subject!r})"
class Cmp(UnaryProp):
def __repr__(self) -> str:
return f"Cmp({self.subject!r})"
class SignedCmp(UnaryProp):
def __repr__(self) -> str:
return f"SignedCmp({self.subject!r})"
class Zero(UnaryProp):
def __repr__(self) -> str:
return f"Zero({self.subject!r})"
class Arith(UnaryProp):
def __repr__(self) -> str:
return f"Arith({self.subject!r})"
class Logic(UnaryProp):
def __repr__(self) -> str:
return f"Logic({self.subject!r})"
def to_cryptol(val : Any, cryptol_type : Optional[CryptolType] = None) -> Any:
if cryptol_type is not None:
return cryptol_type.from_python(val)
else:
return CryptolType().from_python(val)
raise TypeError("Unsupported value: " + str(val))
def fail_with(exn : Exception) -> NoReturn:
raise exn
@ -114,306 +189,153 @@ def is_plausible_json(val : Any) -> bool:
return False
class CryptolType:
def from_python(self, val : Any) -> Any:
if hasattr(val, '__to_cryptol__'):
code = val.__to_cryptol__(self)
if is_plausible_json(code):
return code
else:
raise ValueError(f"Improbable JSON from __to_cryptol__: {val!r} gave {code!r}")
# if isinstance(code, CryptolCode):
# return self.convert(code)
# else:
# raise ValueError(f"Expected Cryptol code from __to_cryptol__ on {val!r}, but got {code!r}.")
else:
return self.convert(val)
def convert(self, val : Any) -> Any:
if isinstance(val, bool):
return val
elif isinstance(val, tuple) and val == ():
return {'expression': 'unit'}
elif isinstance(val, tuple):
return {'expression': 'tuple',
'data': [to_cryptol(x) for x in val]}
elif isinstance(val, dict):
return {'expression': 'record',
'data': {k : to_cryptol(val[k])
if isinstance(k, str)
else fail_with (TypeError("Record keys must be strings"))
for k in val}}
elif isinstance(val, int):
return val
elif isinstance(val, list):
return {'expression': 'sequence',
'data': [to_cryptol(v) for v in val]}
elif isinstance(val, bytes) or isinstance(val, bytearray):
return {'expression': 'bits',
'encoding': 'base64',
'width': 8 * len(val),
'data': base64.b64encode(val).decode('ascii')}
elif isinstance(val, BitVector.BitVector):
n = int(val)
byte_width = ceil(n.bit_length()/8)
return {'expression': 'bits',
'encoding': 'base64',
'width': val.length(), # N.B. original length, not padded
'data': base64.b64encode(n.to_bytes(byte_width,'big')).decode('ascii')}
elif isinstance(val, BV):
return {'expression': 'bits',
'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))
# -----------------------------------------------------------
# Cryptol kinds
# -----------------------------------------------------------
class Var(CryptolType):
def __init__(self, name : str, kind : CryptolKind) -> None:
self.name = name
self.kind = kind
@dataclass
class CryptolArrowKind:
domain : CryptolKind
range : CryptolKind
def __repr__(self) -> str:
return f"Var({self.name!r}, {self.kind!r})"
CryptolKind = Union[typing_extensions.Literal['Type'],
typing_extensions.Literal['Num'],
typing_extensions.Literal['Prop'],
CryptolArrowKind]
class Function(CryptolType):
def __init__(self, dom : CryptolType, ran : CryptolType) -> None:
self.domain = dom
self.range = ran
def __repr__(self) -> str:
return f"Function({self.domain!r}, {self.range!r})"
class Bitvector(CryptolType):
def __init__(self, width : CryptolType) -> None:
self.width = width
def __repr__(self) -> str:
return f"Bitvector({self.width!r})"
def convert(self, val : Any) -> Any:
# XXX figure out what to do when width is not evenly divisible by 8
if isinstance(val, int):
w = eval_numeric(self.width, None)
if w is not None:
return self.convert(int.to_bytes(val, int(w / 8), 'big', signed=True))
else:
raise ValueError(f"Insufficent type information to serialize int as bitvector")
elif isinstance(val, bytearray) or isinstance(val, bytes):
return {'expression': 'bits',
'encoding': 'base64',
'width': eval_numeric(self.width, 8 * len(val)),
'data': base64.b64encode(val).decode('ascii')}
elif isinstance(val, BitVector.BitVector):
return CryptolType.convert(self, val)
elif isinstance(val, BV):
return CryptolType.convert(self, val)
else:
raise ValueError(f"Not supported as bitvector: {val!r}")
def eval_numeric(t : Any, default : A) -> Union[int, A]:
if isinstance(t, Num):
return t.number
def to_kind(k : Any) -> CryptolKind:
if k == "Type": return "Type"
elif k == "Num": return "Num"
elif k == "Prop": return "Prop"
elif k['kind'] == "arrow":
return CryptolArrowKind(k['from'], k['to'])
else:
return default
raise ValueError(f'Not a Cryptol kind: {k!r}')
# -----------------------------------------------------------
# Cryptol types
# -----------------------------------------------------------
class CryptolType:
def from_python(self, val : Any) -> NoReturn:
raise Exception("CryptolType.from_python is deprecated, use to_cryptol")
def convert(self, val : Any) -> NoReturn:
raise Exception("CryptolType.convert is deprecated, use to_cryptol")
@dataclass
class Var(CryptolType):
name : str
kind : CryptolKind
def __str__(self) -> str:
return self.name
@dataclass
class Function(CryptolType):
domain : CryptolType
range : CryptolType
def __str__(self) -> str:
return f"({self.domain} -> {self.range})"
@dataclass
class Bitvector(CryptolType):
width : CryptolType
def __str__(self) -> str:
return f"[{self.width}]"
@dataclass
class Num(CryptolType):
def __init__(self, number : int) -> None:
self.number = number
number : int
def __repr__(self) -> str:
return f"Num({self.number!r})"
def __str__(self) -> str:
return str(self.number)
@dataclass
class Bit(CryptolType):
def __init__(self) -> None:
pass
def __repr__(self) -> str:
return f"Bit()"
def __str__(self) -> str:
return "Bit"
@dataclass
class Sequence(CryptolType):
def __init__(self, length : CryptolType, contents : CryptolType) -> None:
self.length = length
self.contents = contents
length : CryptolType
contents : CryptolType
def __repr__(self) -> str:
return f"Sequence({self.length!r}, {self.contents!r})"
def __str__(self) -> str:
return f"[{self.length}]{self.contents}"
@dataclass
class Inf(CryptolType):
def __repr__(self) -> str:
return f"Inf()"
def __str__(self) -> str:
return "inf"
@dataclass
class Integer(CryptolType):
def __repr__(self) -> str:
return f"Integer()"
def __str__(self) -> str:
return "Integer"
@dataclass
class Rational(CryptolType):
def __repr__(self) -> str:
return f"Rational()"
def __str__(self) -> str:
return "Rational"
@dataclass
class Z(CryptolType):
def __init__(self, modulus : CryptolType) -> None:
self.modulus = modulus
def __repr__(self) -> str:
return f"Z({self.modulus!r})"
class Plus(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
modulus : CryptolType
def __str__(self) -> str:
return f"({self.left} + {self.right})"
return f"(Z {self.modulus})"
@dataclass
class TypeOp(CryptolType):
op : str
args : typing.Sequence[CryptolType]
# we override the @dataclass __init__ and __repr__ because we want the
# syntax of variable numbers of arguments
def __init__(self, op : str, *args : CryptolType) -> None:
self.op = op
self.args = args
def __repr__(self) -> str:
return f"Plus({self.left!r}, {self.right!r})"
class Minus(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
return "TypeOp(" + ", ".join(map(repr, [self.op, *self.args])) + ")"
def __str__(self) -> str:
return f"({self.left} - {self.right})"
def __repr__(self) -> str:
return f"Minus({self.left!r}, {self.right!r})"
class Times(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"({self.left} * {self.right})"
def __repr__(self) -> str:
return f"Times({self.left!r}, {self.right!r})"
class Div(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"({self.left} / {self.right})"
def __repr__(self) -> str:
return f"Div({self.left!r}, {self.right!r})"
class CeilDiv(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"({self.left} /^ {self.right})"
def __repr__(self) -> str:
return f"CeilDiv({self.left!r}, {self.right!r})"
class Mod(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"({self.left} % {self.right})"
def __repr__(self) -> str:
return f"Mod({self.left!r}, {self.right!r})"
class CeilMod(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"({self.left} %^ {self.right})"
def __repr__(self) -> str:
return f"CeilMod({self.left!r}, {self.right!r})"
class Expt(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"({self.left} ^^ {self.right})"
def __repr__(self) -> str:
return f"Expt({self.left!r}, {self.right!r})"
class Log2(CryptolType):
def __init__(self, operand : CryptolType) -> None:
self.operand = operand
def __str__(self) -> str:
return f"(lg2 {self.operand})"
def __repr__(self) -> str:
return f"Log2({self.operand!r})"
class Width(CryptolType):
def __init__(self, operand : CryptolType) -> None:
self.operand = operand
def __str__(self) -> str:
return f"(width {self.operand})"
def __repr__(self) -> str:
return f"Width({self.operand!r})"
class Max(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"(max {self.left} {self.right})"
def __repr__(self) -> str:
return f"Max({self.left!r}, {self.right!r})"
class Min(CryptolType):
def __init__(self, left : CryptolType, right : CryptolType) -> None:
self.left = left
self.right = right
def __str__(self) -> str:
return f"(min {self.left} {self.right})"
def __repr__(self) -> str:
return f"Min({self.left!r}, {self.right!r})"
if self.op.isalnum():
return "(" + " ".join(map(str, [self.op, self.args])) + ")"
elif len(self.args) == 2:
return f"({self.args[0]} {self.op} {self.args[1]})"
else:
raise NotImplementedError(f"__str__ for: {self!r}")
@dataclass
class Tuple(CryptolType):
types : Iterable[CryptolType]
types : typing.Sequence[CryptolType]
# we override the @dataclass __init__ and __repr__ because we want the
# syntax of variable numbers of arguments
def __init__(self, *types : CryptolType) -> None:
self.types = types
def __repr__(self) -> str:
return "Tuple(" + ", ".join(map(str, self.types)) + ")"
return "Tuple(" + ", ".join(map(repr, self.types)) + ")"
def __str__(self) -> str:
return "(" + ",".join(map(str, self.types)) + ")"
@dataclass
class Record(CryptolType):
def __init__(self, fields : Dict[str, CryptolType]) -> None:
self.fields = fields
def __repr__(self) -> str:
return f"Record({self.fields!r})"
fields : Dict[str, CryptolType]
def __str__(self) -> str:
return "{" + ",".join(str(k) + " = " + str(self.fields[k]) for k in self.fields) + "}"
def to_type(t : Any) -> CryptolType:
"""Convert a Cryptol JSON type to a ``CryptolType``."""
if t['type'] == 'variable':
return Var(t['name'], to_kind(t['kind']))
elif t['type'] == 'function':
@ -428,32 +350,10 @@ def to_type(t : Any) -> CryptolType:
return Sequence(to_type(t['length']), to_type(t['contents']))
elif t['type'] == 'inf':
return Inf()
elif t['type'] == '+':
return Plus(*map(to_type, t['arguments']))
elif t['type'] == '-':
return Minus(*map(to_type, t['arguments']))
elif t['type'] == '*':
return Times(*map(to_type, t['arguments']))
elif t['type'] == '/':
return Div(*map(to_type, t['arguments']))
elif t['type'] == '/^':
return CeilDiv(*map(to_type, t['arguments']))
elif t['type'] == '%':
return Mod(*map(to_type, t['arguments']))
elif t['type'] == '%^':
return CeilMod(*map(to_type, t['arguments']))
elif t['type'] == '^^':
return Expt(*map(to_type, t['arguments']))
elif t['type'] == 'lg2':
return Log2(*map(to_type, t['arguments']))
elif t['type'] == 'width':
return Width(*map(to_type, t['arguments']))
elif t['type'] == 'max':
return Max(*map(to_type, t['arguments']))
elif t['type'] == 'min':
return Min(*map(to_type, t['arguments']))
elif t['type'] == 'tuple':
return Tuple(*map(to_type, t['contents']))
elif t['type'] == 'unit':
return Tuple()
elif t['type'] == 'record':
return Record({k : to_type(t['fields'][k]) for k in t['fields']})
elif t['type'] == 'Integer':
@ -462,45 +362,112 @@ def to_type(t : Any) -> CryptolType:
return Rational()
elif t['type'] == 'Z':
return Z(to_type(t['modulus']))
elif 'arguments' in t:
return TypeOp(t['type'], *map(to_type, t['arguments']))
else:
raise NotImplementedError(f"to_type({t!r})")
class CryptolTypeSchema:
def __init__(self,
variables : OrderedDict[str, CryptolKind],
propositions : List[Optional[CryptolProp]], # TODO complete me!
body : CryptolType) -> None:
self.variables = variables
self.propositions = propositions
self.body = body
# -----------------------------------------------------------
# Cryptol props
# -----------------------------------------------------------
class CryptolProp:
pass
@dataclass
class PropCon(CryptolProp):
con : str
args : typing.Sequence[CryptolType]
# we override the @dataclass __init__ and __repr__ because we want the
# syntax of variable numbers of arguments
def __init__(self, con : str, *args : CryptolType) -> None:
self.con = con
self.args = args
def __repr__(self) -> str:
return f"CryptolTypeSchema({self.variables!r}, {self.propositions!r}, {self.body!r})"
return "PropCon(" + ", ".join(map(repr, [self.con, *self.args])) + ")"
def __str__(self) -> str:
if self.con.isalnum():
return "(" + " ".join(map(str, [self.con, self.args])) + ")"
elif len(self.args) == 2:
return f"({self.args[0]} {self.con} {self.args[1]})"
else:
raise NotImplementedError(f"__str__ for: {self!r}")
@dataclass
class And(CryptolProp):
left : CryptolProp
right : CryptolProp
def __str__(self) -> str:
return f"({self.left} && {self.right})"
@dataclass
class TrueProp(CryptolProp):
def __str__(self) -> str:
return "True"
def to_prop(obj : Any) -> CryptolProp:
"""Convert a Cryptol JSON proposition to a ``CryptolProp``."""
if obj['prop'] == 'And':
return And(to_prop(obj['left']), to_prop(obj['right']))
elif obj['prop'] == 'True':
return TrueProp()
# special cases for props which have irregular JSON structure
elif obj['prop'] == 'Literal':
return PropCon('Literal', to_type(obj['size']), to_type(obj['subject']))
elif obj['prop'] == '>=':
return PropCon('>=', to_type(obj['greater']), to_type(obj['less']))
# general cases for unary, binary, and unknown props
elif 'subject' in obj and len(obj) == 2:
return PropCon(obj['prop'], to_type(obj['subject']))
elif 'left' in obj and 'right' in obj and len(obj) == 3:
return PropCon(obj['prop'], to_type(obj['left']), to_type(obj['right']))
elif obj['prop'] == 'unknown':
return PropCon(obj['constructor'], *map(to_type, obj['arguments']))
else:
raise NotImplementedError(f"to_prop({obj!r})")
# -----------------------------------------------------------
# Cryptol type schema
# -----------------------------------------------------------
@dataclass
class CryptolTypeSchema:
variables : OrderedDict[str, CryptolKind]
propositions : List[CryptolProp]
body : CryptolType
def __str__(self) -> str:
vstr, pstr = "", "()"
if len(self.variables) > 0:
vstr = "{" + ", ".join(self.variables.keys()) + "} "
if len(self.propositions) > 0:
pstr = "(" + ", ".join(map(str, self.propositions)) + ")"
return vstr + pstr + " => " + str(self.body)
def to_schema(obj : Any) -> CryptolTypeSchema:
"""Convert a Cryptol JSON type schema to a ``CryptolTypeSchema``."""
return CryptolTypeSchema(OrderedDict((v['name'], to_kind(v['kind']))
for v in obj['forall']),
[to_prop(p) for p in obj['propositions']],
to_type(obj['type']))
def to_prop(obj : Any) -> Optional[CryptolProp]:
if obj['prop'] == 'fin':
return Fin(to_type(obj['subject']))
elif obj['prop'] == 'Cmp':
return Cmp(to_type(obj['subject']))
elif obj['prop'] == 'SignedCmp':
return SignedCmp(to_type(obj['subject']))
elif obj['prop'] == 'Zero':
return Zero(to_type(obj['subject']))
elif obj['prop'] == 'Arith':
return Arith(to_type(obj['subject']))
elif obj['prop'] == 'Logic':
return Logic(to_type(obj['subject']))
def to_schema_or_type(obj : Any) -> Union[CryptolTypeSchema, CryptolType]:
"""Convert a Cryptol JSON type schema to a ``CryptolType`` if it has no
variables or propositions, or to a ``CryptolTypeSchema`` otherwise."""
if 'forall' in obj and 'propositions' in obj and len(obj['forall']) > 0 and len(obj['propositions']) > 0:
return to_schema(obj)
else:
return None
#raise ValueError(f"Can't convert to a Cryptol prop: {obj!r}")
return to_type(obj['type'])
def argument_types(obj : Union[CryptolTypeSchema, CryptolType]) -> List[CryptolType]:
"""Given a ``CryptolTypeSchema` or ``CryptolType`` of a function, return
the types of its arguments."""
if isinstance(obj, CryptolTypeSchema):
return argument_types(obj.body)
elif isinstance(obj, Function):

79
cryptol-remote-api/python/cryptol/custom_fstring.py Normal file
View File

@ -0,0 +1,79 @@
"""An interface for defining custom f-string wrappers"""
from typing import Any, Callable, Dict, List
import builtins
import ast
import sys
def customf(body : str, onAST : Callable[[ast.FormattedValue], List[ast.expr]],
globals : Dict[str, Any] = {}, locals : Dict[str, Any] = {},
*, frames : int = 0, filename : str = "<custom f-string>") -> str:
"""This function parses the given string as if it were an f-string,
applies the given function to the AST of each of the formatting fields in
the string, then evaluates the result to get the resulting string.
By default, the global and local variables used in the call to ``eval``
are the value of ``sys.__getframe(1+frames).f_globals`` and the value of
``sys.__getframe(1+frames).f_locals``, respectively. This is meant to
ensure that the all the variables which were in scope when the custom
f-string is formed are also in scope when it is evaluated. Thus, the value
of ``frames`` should be incremented for each wrapper function defined
around this function (e.g. see the definition of ``func_customf``).
To add additional global or local variable values (which are combined with,
but take precedence over, the values mentioned in the previous paragraph)
use the ``globals`` and ``locals`` keyword arguments.
"""
# Get the global/local variable context of the previous frame so the local
# names 'body', 'onAST', etc. aren't shadowed our the call to ``eval``
previous_frame = sys._getframe(1 + frames)
all_globals = {**previous_frame.f_globals, **globals}
all_locals = {**previous_frame.f_locals, **locals}
# The below line should be where any f-string syntax errors are raised
tree = ast.parse('f' + str(repr(body)), filename=filename, mode='eval')
if not isinstance(tree, ast.Expression) or not isinstance(tree.body, ast.JoinedStr):
raise ValueError(f'Invalid custom f-string: {str(repr(body))}')
joined_values : List[ast.expr] = []
for node in tree.body.values:
if isinstance(node, ast.FormattedValue):
joined_values += onAST(node)
else:
joined_values += [node]
tree.body.values = joined_values
try:
return str(eval(compile(tree, filename=filename, mode='eval'), all_globals, all_locals))
except SyntaxError as e:
# I can't think of a case where we would raise an error here, but if
# we do it's worth telling the user that the column numbers are all
# messed up
msg = '\nNB: Column numbers refer to positions in the original string'
raise type(e)(str(e) + msg).with_traceback(sys.exc_info()[2])
def func_customf(body : str, func : Callable,
globals : Dict[str, Any] = {}, locals : Dict[str, Any] = {},
*, frames : int = 0, filename : str = "<custom f-string>",
doConvFmtAfter : bool = False,
func_id : str = "_func_customf__func_id") -> str:
"""Like ``customf``, but can be provided a function to apply to the values
of each of the formatting fields before they are formatted as strings,
instead of a function applied to their ASTs.
Unless the parameter ``doConvFmtAfter`` is set to ``True``, any conversions
(i.e. ``{...!s}``, ``{...!r}``, or ``{...!a}``) or format specifiers
(e.g. ``{...:>30}`` or ``{...:+f}``) in the input string will be applied
before the given function is applied. For example,
``func_customf('{5!r}', f)`` is the same as ``f'{f(repr(5))}'``, but
``func_customf('{5!r}', f, doConvFmtAfter=True)`` is ``f'{repr(f(5))}'``.
"""
def onAST(node : ast.FormattedValue) -> List[ast.expr]:
kwargs = {'lineno': node.lineno, 'col_offset': node.col_offset}
func = ast.Name(id=func_id, ctx=ast.Load(), **kwargs)
if doConvFmtAfter or (node.conversion == -1 and node.format_spec is None):
node.value = ast.Call(func=func, args=[node.value], keywords=[], **kwargs)
else:
node_str = ast.JoinedStr(values=[node], **kwargs)
node_val = ast.Call(func=func, args=[node_str], keywords=[], **kwargs)
node = ast.FormattedValue(value=node_val, conversion=-1, format_spec=None, **kwargs)
return [node]
return customf(body, onAST, globals, {**locals, func_id:func}, frames=1+frames,
filename=filename)

18
cryptol-remote-api/python/cryptol/opaque.py
View File

@ -1,5 +1,8 @@
from typing import Any
from dataclasses import dataclass
# we freeze this class because ``OpaqueValue``s represent immutable objects
@dataclass(frozen=True)
class OpaqueValue():
"""A value from the Cryptol server which cannot be directly represented and/or
marshalled to an RPC client.
@ -9,20 +12,5 @@ class OpaqueValue():
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)

84
cryptol-remote-api/python/cryptol/quoting.py Normal file
View File

@ -0,0 +1,84 @@
"""Cryptol quasiquotation using an f-string-like syntax"""
from typing import Any, Union
from .bitvector import BV
from .opaque import OpaqueValue
from .commands import CryptolValue
from .cryptoltypes import CryptolJSON, CryptolLiteral, parenthesize
from .custom_fstring import *
def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str:
"""Converts a ``CryptolValue``, string literal, or ``CryptolJSON`` into
a string of Cryptol syntax."""
if isinstance(val, bool):
return 'True' if val else 'False'
elif isinstance(val, tuple):
return '(' + ', '.join(to_cryptol_str(x) for x in val) + ')'
elif isinstance(val, dict):
return '{' + ', '.join(f'{k} = {to_cryptol_str(v)}' for k,v in val.items()) + '}'
elif isinstance(val, int):
return str(val)
elif isinstance(val, list):
return '[' + ', '.join(to_cryptol_str(x) for x in val) + ']'
elif isinstance(val, BV):
if val.size() % 4 == 0:
return val.hex()
else:
return f'({val.to_signed_int()} : [{val.size()}])'
elif isinstance(val, OpaqueValue):
return str(val)
elif isinstance(val, str):
return f'"{val}"'
elif hasattr(val, '__to_cryptol_str__'):
return parenthesize(val.__to_cryptol_str__())
else:
raise TypeError("Unable to convert value to Cryptol syntax: " + str(val))
def to_cryptol_str_customf(s : str, *, frames : int = 0,
filename : str = "<cry_f>") -> str:
"""The function used to parse strings given to ``cry_f``"""
return func_customf(s, to_cryptol_str, frames=1+frames,
filename=filename)
def cry(s : str) -> CryptolLiteral:
"""Embed a string of Cryptol syntax as ``CryptolCode``"""
return CryptolLiteral(s)
def cry_f(s : str) -> CryptolLiteral:
"""Embed a string of Cryptol syntax as ``CryptolCode``, where the given
string is parsed as an f-string, and the values within brackets are
converted to Cryptol syntax using ``to_cryptol_str``.
Like f-strings, values in brackets (``{``, ``}``) are parsed as python
expressions in the caller's context of local and global variables, and
to include a literal bracket in the final string, it must be doubled
(i.e. ``{{`` or ``}}``). The latter is needed when using explicit type
application or record syntax. For example, if ``x = [0,1]`` then
``cry_f('length `{{2}} {x}')`` is equal to ``cry('length `{2} [0,1]')``
and ``cry_f('{{ x = {x} }}')`` is equal to ``cry('{ x = [0,1] }')``.
When formatting Cryptol, it is recomended to use this function rather
than any of python's built-in methods of string formatting (e.g.
f-strings, ``str.format``) as the latter will not always produce valid
Cryptol syntax. Specifically, this function differs from these methods
in the cases of ``BV``s, string literals, function application (this
function will add parentheses as needed), and dicts. For example,
``cry_f('{ {"x": 5, "y": 4} }')`` equals ``cry('{x = 5, y = 4}')``
but ``f'{ {"x": 5, "y": 4} }'`` equals ``'{"x": 5, "y": 4}'``. Only
the former is valid Cryptol syntax for a record.
Note that any conversion or format specifier will always result in the
argument being rendered as a Cryptol string literal with the conversion
and/or formating applied. For example, `cry('f {5}')` is equal to
``cry('f 5')`` but ``cry_f('f {5!s}')`` is equal to ``cry(`f "5"`)``
and ``cry_f('f {5:+.2%}')`` is equal to ``cry('f "+500.00%"')``.
:example:
>>> x = BV(size=7, value=1)
>>> y = cry_f('fun1 {x}')
>>> cry_f('fun2 {y}')
'fun2 (fun1 (1 : [7]))'
"""
return CryptolLiteral(to_cryptol_str_customf(s, frames=1))

244
cryptol-remote-api/python/cryptol/single_connection.py Normal file
View File

@ -0,0 +1,244 @@
"""A single-connection, synchronous, typed interface for the Cryptol bindings"""
from __future__ import annotations
import sys
from typing import Any, Optional, Union, List, Dict, TextIO, overload
from typing_extensions import Literal
from .custom_fstring import *
from .quoting import *
from .solver import OfflineSmtQuery, Solver, OnlineSolver, OfflineSolver, Z3
from .connection import CryptolValue, CheckReport
from . import synchronous
from .synchronous import Qed, Safe, Counterexample, Satisfiable, Unsatisfiable
from . import cryptoltypes
__designated_connection = None # type: Optional[synchronous.CryptolSyncConnection]
def __get_designated_connection() -> synchronous.CryptolSyncConnection:
global __designated_connection
if __designated_connection is None:
raise ValueError("There is not yet a designated connection.")
else:
return __designated_connection
def __set_designated_connection(conn: synchronous.CryptolSyncConnection) -> None:
global __designated_connection
__designated_connection = conn
def connected() -> bool:
global __designated_connection
return __designated_connection is not None
def connect(command : Optional[str]=None,
*,
cryptol_path : Optional[str] = None,
url : Optional[str] = None,
reset_server : bool = False,
verify : Union[bool, str] = True,
log_dest : Optional[TextIO] = None,
timeout : Optional[float] = None) -> None:
"""
Connect to a (possibly new) synchronous Cryptol server process.
:param command: A command to launch a new Cryptol server in socket mode (if provided).
:param cryptol_path: A replacement for the contents of
the ``CRYPTOLPATH`` environment variable (if provided).
:param url: A URL at which to connect to an already running Cryptol
HTTP server.
:param reset_server: If ``True``, the server that is connected to will be
reset. (This ensures any states from previous server usages have been
cleared.)
:param verify: Determines whether a secure HTTP connection should verify the SSL certificates.
Corresponds to the ``verify`` keyword parameter on ``requests.post``. N.B.,
only has an affect when ``connect`` is called with a ``url`` parameter
or when the ``CRYPTOL_SERVER_URL`` environment variable is set.
:param log_dest: A destination to log JSON requests/responses to, e.g. ``log_dest=sys.stderr``
will print traffic to ``stderr``, ``log_dest=open('foo.log', 'w')`` will log to ``foo.log``,
etc.
:param timeout: Optional default timeout (in seconds) for methods. Can be modified/read via the
the `get_default_timeout` and `set_default_timeout` methods. Method invocations which specify
the optional `timeout` keyword parameter will cause the default to be ignored for that method.
If no ``command`` or ``url`` parameters are provided, the following are attempted in order:
1. If the environment variable ``CRYPTOL_SERVER`` is set and referse to an executable,
it is assumed to be a Cryptol server and will be used for a new ``socket`` connection.
2. If the environment variable ``CRYPTOL_SERVER_URL`` is set, it is assumed to be
the URL for a running Cryptol server in ``http`` mode and will be connected to.
3. If an executable ``cryptol-remote-api`` is available on the ``PATH``
it is assumed to be a Cryptol server and will be used for a new ``socket`` connection.
"""
global __designated_connection
__set_designated_connection(synchronous.connect(
command=command,
cryptol_path=cryptol_path,
url=url,
reset_server=reset_server,
verify=verify,
log_dest=log_dest,
timeout=timeout))
def connect_stdio(command : str,
cryptol_path : Optional[str] = None,
log_dest : Optional[TextIO] = None,
timeout : Optional[float] = None) -> None:
"""Start a new synchronous connection to a new Cryptol server process.
:param command: The command to launch the Cryptol server.
:param cryptol_path: An optional replacement for the contents of
the ``CRYPTOLPATH`` environment variable.
:param log_dest: A destination to log JSON requests/responses to, e.g. ``log_dest=sys.stderr``
will print traffic to ``stderr``, ``log_dest=open('foo.log', 'w')`` will log to ``foo.log``,
etc.
:param timeout: Optional default timeout (in seconds) for methods. Can be modified/read via the
the `get_default_timeout` and `set_default_timeout` methods. Method invocations which specify
the optional `timeout` keyword parameter will cause the default to be ignored for that method.
"""
__set_designated_connection(synchronous.connect_stdio(
command=command,
cryptol_path=cryptol_path,
log_dest=log_dest,
timeout=timeout))
def get_default_timeout() -> Optional[float]:
"""Get the value of the optional default timeout for methods (in seconds)."""
return __get_designated_connection().get_default_timeout()
def set_default_timeout(timeout : Optional[float]) -> None:
"""Set the value of the optional default timeout for methods (in seconds)."""
__get_designated_connection().set_default_timeout(timeout)
def load_file(filename : str, *, timeout:Optional[float] = None) -> None:
"""Load a filename as a Cryptol module, like ``:load`` at the Cryptol
REPL.
"""
__get_designated_connection().load_file(filename, timeout=timeout)
def load_module(module_name : str, *, timeout:Optional[float] = None) -> None:
"""Load a Cryptol module, like ``:module`` at the Cryptol REPL."""
__get_designated_connection().load_module(module_name, timeout=timeout)
def extend_search_path(*dir : str, timeout:Optional[float] = None) -> None:
"""Extend the search path for loading Cryptol modules."""
__get_designated_connection().extend_search_path(*dir, timeout=timeout)
def cry_eval(expression : Any, *, timeout:Optional[float] = None) -> CryptolValue:
"""Evaluate a Cryptol expression, with the result represented
according to :ref:`cryptol-json-expression`, with Python datatypes
standing for their JSON equivalents.
"""
return __get_designated_connection().eval(expression, timeout=timeout)
def cry_eval_f(s : str, *, timeout:Optional[float] = None) -> CryptolValue:
"""Parses the given string like ``cry_f``, then evalues it, with the
result represented according to :ref:`cryptol-json-expression`, with
Python datatypes standing for their JSON equivalents.
"""
expression = to_cryptol_str_customf(s, frames=1, filename="<cry_eval_f>")
return cry_eval(expression, timeout=timeout)
def call(fun : str, *args : List[Any], timeout:Optional[float] = None) -> CryptolValue:
"""Evaluate a Cryptol functiom by name, with the arguments and the
result represented according to :ref:`cryptol-json-expression`, with
Python datatypes standing for their JSON equivalents.
"""
return __get_designated_connection().call(fun, *args, timeout=timeout)
def check(expr : Any, *, num_tests : Union[Literal['all'], int, None] = None, timeout:Optional[float] = None) -> CheckReport:
"""Tests the validity of a Cryptol expression with random inputs. The expression must be a function with
return type ``Bit``.
If ``num_tests`` is ``"all"`` then the expression is tested exhaustively (i.e., against all possible inputs).
If ``num_tests`` is omitted, Cryptol defaults to running 100 tests.
"""
return __get_designated_connection().check(expr, num_tests=num_tests, timeout=timeout)
def check_type(code : Any, *, timeout:Optional[float] = None) -> Union[cryptoltypes.CryptolType, cryptoltypes.CryptolTypeSchema]:
"""Check the type of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents.
"""
return __get_designated_connection().check_type(code, timeout=timeout)
@overload
def sat(expr : Any, solver : OfflineSolver, count : int = 1, *, timeout:Optional[float] = None) -> OfflineSmtQuery: ...
@overload
def sat(expr : Any, solver : OnlineSolver = Z3, count : int = 1, *, timeout:Optional[float] = None) -> Union[Satisfiable, Unsatisfiable]: ...
@overload
def sat(expr : Any, solver : Solver = Z3, count : int = 1, *, timeout:Optional[float] = None) -> Union[Satisfiable, Unsatisfiable, OfflineSmtQuery]: ...
def sat(expr : Any, solver : Solver = Z3, count : int = 1, *, timeout:Optional[float] = None) -> Union[Satisfiable, Unsatisfiable, OfflineSmtQuery]:
"""Check the satisfiability of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`, and return up to
`count` solutions.
"""
return __get_designated_connection().sat(expr, solver, count, timeout=timeout)
@overload
def prove(expr : Any, solver : OfflineSolver, *, timeout:Optional[float] = None) -> OfflineSmtQuery: ...
@overload
def prove(expr : Any, solver : OnlineSolver = Z3, *, timeout:Optional[float] = None) -> Union[Qed, Counterexample]: ...
@overload
def prove(expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Qed, Counterexample, OfflineSmtQuery]: ...
def prove(expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Qed, Counterexample, OfflineSmtQuery]:
"""Check the validity of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`.
"""
return __get_designated_connection().prove(expr, solver, timeout=timeout)
@overload
def safe(expr : Any, solver : OfflineSolver, *, timeout:Optional[float] = None) -> OfflineSmtQuery: ...
@overload
def safe(expr : Any, solver : OnlineSolver = Z3, *, timeout:Optional[float] = None) -> Union[Safe, Counterexample]: ...
@overload
def safe(expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Safe, Counterexample, OfflineSmtQuery]: ...
def safe(expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Safe, Counterexample, OfflineSmtQuery]:
"""Check via an external SMT solver that the given term is safe for all inputs,
which means it cannot encounter a run-time error.
"""
return __get_designated_connection().safe(expr, solver, timeout=timeout)
def names(*, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
"""Discover the list of names currently in scope in the current context."""
return __get_designated_connection().names(timeout=timeout)
def focused_module(*, timeout:Optional[float] = None) -> Dict[str,Any]:
"""Returns the name and other information about the currently-focused module."""
return __get_designated_connection().focused_module(timeout=timeout)
def reset() -> None:
"""Resets the connection, causing its unique state on the server to be freed (if applicable).
After a reset a connection may be treated as if it were a fresh connection with the server if desired."""
__get_designated_connection().reset()
def reset_server() -> None:
"""Resets the Cryptol server, clearing all states."""
__get_designated_connection().reset_server()
def interrupt() -> None:
"""Interrupt the Cryptol server, cancelling any in-progress requests."""
__get_designated_connection().interrupt()
def logging(on : bool, *, dest : TextIO = sys.stderr) -> None:
"""Whether to log received and transmitted JSON."""
__get_designated_connection().logging(on=on,dest=dest)

71
cryptol-remote-api/python/cryptol/solver.py
View File

@ -1,14 +1,23 @@
"""Cryptol solver-related definitions"""
from typing import NewType
from abc import ABCMeta, abstractmethod
from typing import Any
from dataclasses import dataclass
@dataclass
class OfflineSmtQuery():
"""An SMTLIB2 script -- produced when an `offline` prover is used."""
"""An SMTLIB2 script -- produced when an `offline` prover is used. Instances
of this class are neither truthy nor falsy, using an instance of this class
in an 'if' or 'while' statement will result in an error.
"""
content: str
class Solver():
def __bool__(self) -> Any:
raise ValueError("Offline SMT query has no value")
def __nonzero__(self) -> Any:
raise ValueError("Offline SMT query has no value")
class Solver(metaclass=ABCMeta):
"""An SMT solver mode selectable for Cryptol. Compare with the `:set prover` options in
the Cryptol REPL."""
__name: str
@ -27,31 +36,41 @@ class Solver():
"""Returns whether hash consing is enabled (if applicable)."""
return self.__hash_consing
@abstractmethod
def without_hash_consing(self) -> 'Solver':
"""Returns an identical solver but with hash consing disabled (if applicable)."""
return Solver(name=self.__name, hash_consing=False)
pass
class OnlineSolver(Solver):
def without_hash_consing(self) -> 'OnlineSolver':
return OnlineSolver(name=self.name(), hash_consing=False)
class OfflineSolver(Solver):
def without_hash_consing(self) -> 'OfflineSolver':
return OfflineSolver(name=self.name(), hash_consing=False)
# Cryptol-supported SMT configurations/solvers
# (see Cryptol.Symbolic.SBV Haskell module)
CVC4: Solver = Solver("cvc4")
YICES: Solver = Solver("yices")
Z3: Solver = Solver("z3")
BOOLECTOR: Solver = Solver("boolector")
MATHSAT: Solver = Solver("mathsat")
ABC: Solver = Solver("abc")
OFFLINE: Solver = Solver("offline")
ANY: Solver = Solver("any")
SBV_CVC4: Solver = Solver("sbv-cvc4")
SBV_YICES: Solver = Solver("sbv-yices")
SBV_Z3: Solver = Solver("sbv-z3")
SBV_BOOLECTOR: Solver = Solver("sbv-boolector")
SBV_MATHSAT: Solver = Solver("sbv-mathsat")
SBV_ABC: Solver = Solver("sbv-abc")
SBV_OFFLINE: Solver = Solver("sbv-offline")
SBV_ANY: Solver = Solver("sbv-any")
W4_CVC4: Solver = Solver("w4-cvc4")
W4_YICES: Solver = Solver("w4-yices")
W4_Z3: Solver = Solver("w4-z3")
W4_BOOLECTOR: Solver = Solver("w4-boolector")
W4_OFFLINE: Solver = Solver("w4-offline")
W4_ABC: Solver = Solver("w4-any")
CVC4: OnlineSolver = OnlineSolver("cvc4")
YICES: OnlineSolver = OnlineSolver("yices")
Z3: OnlineSolver = OnlineSolver("z3")
BOOLECTOR: OnlineSolver = OnlineSolver("boolector")
MATHSAT: OnlineSolver = OnlineSolver("mathsat")
ABC: OnlineSolver = OnlineSolver("abc")
OFFLINE: OfflineSolver = OfflineSolver("offline")
ANY: OnlineSolver = OnlineSolver("any")
SBV_CVC4: OnlineSolver = OnlineSolver("sbv-cvc4")
SBV_YICES: OnlineSolver = OnlineSolver("sbv-yices")
SBV_Z3: OnlineSolver = OnlineSolver("sbv-z3")
SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
SBV_MATHSAT: OnlineSolver = OnlineSolver("sbv-mathsat")
SBV_ABC: OnlineSolver = OnlineSolver("sbv-abc")
SBV_OFFLINE: OfflineSolver = OfflineSolver("sbv-offline")
SBV_ANY: OnlineSolver = OnlineSolver("sbv-any")
W4_CVC4: OnlineSolver = OnlineSolver("w4-cvc4")
W4_YICES: OnlineSolver = OnlineSolver("w4-yices")
W4_Z3: OnlineSolver = OnlineSolver("w4-z3")
W4_BOOLECTOR: OnlineSolver = OnlineSolver("w4-boolector")
W4_OFFLINE: OfflineSolver = OfflineSolver("w4-offline")
W4_ABC: OnlineSolver = OnlineSolver("w4-abc")
W4_ANY: OnlineSolver = OnlineSolver("w4-any")

381
cryptol-remote-api/python/cryptol/synchronous.py Normal file
View File

@ -0,0 +1,381 @@
"""A synchronous, typed interface for the Cryptol bindings"""
from __future__ import annotations
import sys
from typing import Any, Optional, Union, List, Dict, TextIO, overload
from typing_extensions import Literal
from dataclasses import dataclass
from .custom_fstring import *
from .quoting import *
from .solver import OfflineSmtQuery, Solver, OnlineSolver, OfflineSolver, Z3
from . import connection
from . import cryptoltypes
from .commands import *
from . import CryptolConnection, SmtQueryType
@dataclass
class Qed:
"""The positive result of a 'prove' SMT query. All instances of this class
are truthy, i.e. evaluate to `True` in an 'if' or 'while' statement.
"""
def __bool__(self) -> Literal[True]:
return True
def __nonzero__(self) -> Literal[True]:
return True
@dataclass
class Safe:
"""The positive result of a 'safe' SMT query. All instances of this class
are truthy, i.e. evaluate to `True` in an 'if' or 'while' statement.
"""
def __bool__(self) -> Literal[True]:
return True
def __nonzero__(self) -> Literal[True]:
return True
@dataclass
class Counterexample:
"""The negative result of a 'prove' or 'safe' SMT query, consisting of a
type (either "predicate falsified" or "safety violation") and the list of
values which constitute the counterexample. All instances of this class are
falsy, i.e. evaluate to `False` in an 'if' or 'while' statement. (Note that
this is different from the behaivor of a plain list, which is truthy iff
it has nonzero length.)
"""
type : Union[Literal["predicate falsified"], Literal["safety violation"]]
assignments : List[CryptolValue]
def __bool__(self) -> Literal[False]:
return False
def __nonzero__(self) -> Literal[False]:
return False
@dataclass
class Satisfiable:
"""The positive result of a 'sat' SMT query, consisting of a list of
models, where each model is a list of values satisfying the predicate.
All instances of this class are truthy, i.e. evaluate to `True` in an 'if'
or 'while' statement. (Note that this is different from the behaivor of a
plain list, which is truthy iff it has nonzero length.)
"""
models : List[List[CryptolValue]]
def __bool__(self) -> Literal[True]:
return True
def __nonzero__(self) -> Literal[True]:
return True
@dataclass
class Unsatisfiable:
"""The negative result of a 'sat' SMT query. All instances of this class
are falsy, i.e. evaluate to `False` in an 'if 'or 'while' statement.
"""
def __bool__(self) -> Literal[False]:
return False
def __nonzero__(self) -> Literal[False]:
return False
def connect(command : Optional[str]=None,
*,
cryptol_path : Optional[str] = None,
url : Optional[str] = None,
reset_server : bool = False,
verify : Union[bool, str] = True,
log_dest : Optional[TextIO] = None,
timeout : Optional[float] = None) -> CryptolSyncConnection:
"""
Connect to a (possibly new) synchronous Cryptol server process.
:param command: A command to launch a new Cryptol server in socket mode (if provided).
:param cryptol_path: A replacement for the contents of
the ``CRYPTOLPATH`` environment variable (if provided).
:param url: A URL at which to connect to an already running Cryptol
HTTP server.
:param reset_server: If ``True``, the server that is connected to will be
reset. (This ensures any states from previous server usages have been
cleared.)
:param verify: Determines whether a secure HTTP connection should verify the SSL certificates.
Corresponds to the ``verify`` keyword parameter on ``requests.post``. N.B.,
only has an affect when ``connect`` is called with a ``url`` parameter
or when the ``CRYPTOL_SERVER_URL`` environment variable is set.
:param log_dest: A destination to log JSON requests/responses to, e.g. ``log_dest=sys.stderr``
will print traffic to ``stderr``, ``log_dest=open('foo.log', 'w')`` will log to ``foo.log``,
etc.
:param timeout: Optional default timeout (in seconds) for methods. Can be modified/read via the
`timeout` property on a `CryptolSyncConnection` or the `get_default_timeout` and
`set_default_timeout` methods. Method invocations which specify the optional `timeout` keyword
parameter will cause the default to be ignored for that method.
If no ``command`` or ``url`` parameters are provided, the following are attempted in order:
1. If the environment variable ``CRYPTOL_SERVER`` is set and referse to an executable,
it is assumed to be a Cryptol server and will be used for a new ``socket`` connection.
2. If the environment variable ``CRYPTOL_SERVER_URL`` is set, it is assumed to be
the URL for a running Cryptol server in ``http`` mode and will be connected to.
3. If an executable ``cryptol-remote-api`` is available on the ``PATH``
it is assumed to be a Cryptol server and will be used for a new ``socket`` connection.
"""
return CryptolSyncConnection(connection.connect(
command=command,
cryptol_path=cryptol_path,
url=url,
reset_server=reset_server,
verify=verify,
log_dest=log_dest,
timeout=timeout))
def connect_stdio(command : str,
cryptol_path : Optional[str] = None,
log_dest : Optional[TextIO] = None,
timeout : Optional[float] = None) -> CryptolSyncConnection:
"""Start a new synchronous connection to a new Cryptol server process.
:param command: The command to launch the Cryptol server.
:param cryptol_path: An optional replacement for the contents of
the ``CRYPTOLPATH`` environment variable.
:param log_dest: A destination to log JSON requests/responses to, e.g. ``log_dest=sys.stderr``
will print traffic to ``stderr``, ``log_dest=open('foo.log', 'w')`` will log to ``foo.log``,
etc.
:param timeout: Optional default timeout (in seconds) for methods. Can be modified/read via the
`timeout` property on a `CryptolSyncConnection` or the `get_default_timeout` and
`set_default_timeout` methods. Method invocations which specify the optional `timeout` keyword
parameter will cause the default to be ignored for that method.
"""
return CryptolSyncConnection(connection.connect_stdio(
command=command,
cryptol_path=cryptol_path,
log_dest=log_dest,
timeout=timeout))
class CryptolSyncConnection:
"""A wrapper of ``CryptolConnection`` with a synchronous, typed interface."""
connection : CryptolConnection
def __init__(self, connection : CryptolConnection):
self.connection = connection
@property
def timeout(self) -> Optional[float]:
return self.connection.timeout
@timeout.setter
def timeout(self, timeout : Optional[float]) -> None:
self.connection.timeout = timeout
def get_default_timeout(self) -> Optional[float]:
"""Get the value of the optional default timeout for methods (in seconds)."""
return self.connection.get_default_timeout()
def set_default_timeout(self, timeout : Optional[float]) -> None:
"""Set the value of the optional default timeout for methods (in seconds)."""
self.connection.set_default_timeout(timeout)
def load_file(self, filename : str, *, timeout:Optional[float] = None) -> None:
"""Load a filename as a Cryptol module, like ``:load`` at the Cryptol
REPL.
"""
self.connection.load_file(filename, timeout=timeout).result()
def load_module(self, module_name : str, *, timeout:Optional[float] = None) -> None:
"""Load a Cryptol module, like ``:module`` at the Cryptol REPL."""
self.connection.load_module(module_name, timeout=timeout).result()
def extend_search_path(self, *dir : str, timeout:Optional[float] = None) -> None:
"""Extend the search path for loading Cryptol modules."""
self.connection.extend_search_path(*dir, timeout=timeout).result()
def eval(self, expression : Any, *, timeout:Optional[float] = None) -> CryptolValue:
"""Evaluate a Cryptol expression, with the result represented
according to :ref:`cryptol-json-expression`, with Python datatypes
standing for their JSON equivalents.
"""
return from_cryptol_arg(self.connection.eval_raw(expression, timeout=timeout).result())
def eval_f(self, s : str, *, timeout:Optional[float] = None) -> CryptolValue:
"""Parses the given string like ``cry_f``, then evalues it, with the
result represented according to :ref:`cryptol-json-expression`, with
Python datatypes standing for their JSON equivalents.
"""
expression = to_cryptol_str_customf(s, frames=1, filename="<eval_f>")
return self.eval(expression, timeout=timeout)
def call(self, fun : str, *args : List[Any], timeout:Optional[float] = None) -> CryptolValue:
"""Evaluate a Cryptol functiom by name, with the arguments and the
result represented according to :ref:`cryptol-json-expression`, with
Python datatypes standing for their JSON equivalents.
"""
return from_cryptol_arg(self.connection.call_raw(fun, *args, timeout=timeout).result())
def check(self, expr : Any, *, num_tests : Union[Literal['all'], int, None] = None, timeout:Optional[float] = None) -> CheckReport:
"""Tests the validity of a Cryptol expression with random inputs. The expression must be a function with
return type ``Bit``.
If ``num_tests`` is ``"all"`` then the expression is tested exhaustively (i.e., against all possible inputs).
If ``num_tests`` is omitted, Cryptol defaults to running 100 tests.
"""
return to_check_report(self.connection.check_raw(expr, num_tests=num_tests, timeout=timeout).result())
def check_type(self, code : Any, *, timeout:Optional[float] = None) -> Union[cryptoltypes.CryptolType, cryptoltypes.CryptolTypeSchema]:
"""Check the type of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents.
"""
return cryptoltypes.to_schema_or_type(self.connection.check_type(code, timeout=timeout).result())
@overload
def sat(self, expr : Any, solver : OfflineSolver, count : int = 1, *, timeout:Optional[float] = None) -> OfflineSmtQuery: ...
@overload
def sat(self, expr : Any, solver : OnlineSolver = Z3, count : int = 1, *, timeout:Optional[float] = None) -> Union[Satisfiable, Unsatisfiable]: ...
@overload
def sat(self, expr : Any, solver : Solver = Z3, count : int = 1, *, timeout:Optional[float] = None) -> Union[Satisfiable, Unsatisfiable, OfflineSmtQuery]: ...
def sat(self, expr : Any, solver : Solver = Z3, count : int = 1, *, timeout:Optional[float] = None) -> Union[Satisfiable, Unsatisfiable, OfflineSmtQuery]:
"""Check the satisfiability of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`, and return up to
`count` solutions.
If the given solver is an `OnlineSolver`, the result is either an
instance of `Satisfiable`, which is always truthy, or `Unsatisfiable`,
which is always falsy - meaning the result will evaluate to `True` in
an 'if' or 'while' statement iff the given expression is satisfiable.
If the given solver is an `OfflineSolver`, an error will be raised if
the result is used in an 'if' or 'while' statement.
"""
if isinstance(solver, OfflineSolver):
res = self.connection.sat_raw(expr, solver, count, timeout=timeout).result()
if res['result'] == 'offline':
return OfflineSmtQuery(res['query'])
else:
raise ValueError("Expected an offline SMT result, got: " + str(res))
elif isinstance(solver, OnlineSolver):
res = self.connection.sat_raw(expr, solver, count, timeout=timeout).result()
if res['result'] == 'unsatisfiable':
return Unsatisfiable()
elif res['result'] == 'satisfied':
return Satisfiable([[from_cryptol_arg(arg['expr']) for arg in m] for m in res['models']])
else:
raise ValueError("Unexpected 'sat' SMT result: " + str(res))
else:
raise ValueError("Unknown solver type: " + str(solver))
@overload
def prove(self, expr : Any, solver : OfflineSolver, *, timeout:Optional[float] = None) -> OfflineSmtQuery: ...
@overload
def prove(self, expr : Any, solver : OnlineSolver = Z3, *, timeout:Optional[float] = None) -> Union[Qed, Counterexample]: ...
@overload
def prove(self, expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Qed, Counterexample, OfflineSmtQuery]: ...
def prove(self, expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Qed, Counterexample, OfflineSmtQuery]:
"""Check the validity of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`.
If the given solver is an `OnlineSolver`, the result is either an
instance of `Qed`, which is always truthy, or `Counterexample`, which
is always falsy - meaning the result will evaluate to `True` in an 'if'
or 'while' statement iff the given expression can be proved. If the
given solver is an `OfflineSolver`, an error will be raised if the
result is used in an 'if' or 'while' statement.
"""
if isinstance(solver, OfflineSolver):
res = self.connection.prove_raw(expr, solver, timeout=timeout).result()
if res['result'] == 'offline':
return OfflineSmtQuery(res['query'])
else:
raise ValueError("Expected an offline SMT result, got: " + str(res))
elif isinstance(solver, OnlineSolver):
res = self.connection.prove_raw(expr, solver, timeout=timeout).result()
if res['result'] == 'unsatisfiable':
return Qed()
elif res['result'] == 'invalid':
return Counterexample(res['counterexample type'], [from_cryptol_arg(arg['expr']) for arg in res['counterexample']])
else:
raise ValueError("Unexpected 'prove' SMT result: " + str(res))
else:
raise ValueError("Unknown solver type: " + str(solver))
@overload
def safe(self, expr : Any, solver : OfflineSolver, *, timeout:Optional[float] = None) -> OfflineSmtQuery: ...
@overload
def safe(self, expr : Any, solver : OnlineSolver = Z3, *, timeout:Optional[float] = None) -> Union[Safe, Counterexample]: ...
@overload
def safe(self, expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Safe, Counterexample, OfflineSmtQuery]: ...
def safe(self, expr : Any, solver : Solver = Z3, *, timeout:Optional[float] = None) -> Union[Safe, Counterexample, OfflineSmtQuery]:
"""Check via an external SMT solver that the given term is safe for all inputs,
which means it cannot encounter a run-time error.
If the given solver is an `OnlineSolver`, the result is either an
instance of `Safe`, which is always truthy, or `Counterexample`, which
is always falsy - meaning the result will evaluate to `True` in an 'if'
or 'while' statement iff the given expression is safe. If the given
solver is an `OfflineSolver`, an error will be raised if the result is
used in an 'if' or 'while' statement.
"""
if isinstance(solver, OfflineSolver):
res = self.connection.safe_raw(expr, solver, timeout=timeout).result()
if res['result'] == 'offline':
return OfflineSmtQuery(res['query'])
else:
raise ValueError("Expected an offline SMT result, got: " + str(res))
elif isinstance(solver, OnlineSolver):
res = self.connection.safe_raw(expr, solver, timeout=timeout).result()
if res['result'] == 'unsatisfiable':
return Safe()
elif res['result'] == 'invalid':
return Counterexample(res['counterexample type'], [from_cryptol_arg(arg['expr']) for arg in res['counterexample']])
else:
raise ValueError("Unexpected 'safe' SMT result: " + str(res))
else:
raise ValueError("Unknown solver type: " + str(solver))
def names(self, *, timeout:Optional[float] = None) -> List[Dict[str,Any]]:
"""Discover the list of names currently in scope in the current context."""
res = self.connection.names(timeout=timeout).result()
if isinstance(res, list) and all(isinstance(d, dict) and all(isinstance(k, str) for k in d.keys()) for d in res):
return res
else:
raise ValueError("Panic! Result of `names()` is malformed: " + str(res))
def focused_module(self, *, timeout:Optional[float] = None) -> Dict[str,Any]:
"""Returns the name and other information about the currently-focused module."""
res = self.connection.focused_module(timeout=timeout).result()
if isinstance(res, dict) and all(isinstance(k, str) for k in res.keys()):
return res
else:
raise ValueError("Panic! Result of `focused_module()` is malformed: " + str(res))
def reset(self) -> None:
"""Resets the connection, causing its unique state on the server to be freed (if applicable).
After a reset a connection may be treated as if it were a fresh connection with the server if desired."""
self.connection.reset()
def reset_server(self) -> None:
"""Resets the Cryptol server, clearing all states."""
self.connection.reset_server()
def interrupt(self) -> None:
"""Interrupt the Cryptol server, cancelling any in-progress requests."""
self.connection.interrupt()
def logging(self, on : bool, *, dest : TextIO = sys.stderr) -> None:
"""Whether to log received and transmitted JSON."""
self.connection.server_connection.logging(on=on,dest=dest)

89
cryptol-remote-api/python/poetry.lock generated
View File

@ -1,14 +1,14 @@
[[package]]
name = "argo-client"
version = "0.0.5"
version = "0.0.10"
description = "A JSON RPC client library."
category = "main"
optional = false
python-versions = ">=3.7"
python-versions = ">=3.7.0,<4"
[package.dependencies]
mypy = "*"
requests = "*"
requests = ">=2.26.0,<3.0.0"
urllib3 = ">=1.26.5"
[[package]]
name = "bitvector"
@ -20,33 +20,36 @@ python-versions = "*"
[[package]]
name = "certifi"
version = "2021.5.30"
version = "2021.10.8"
description = "Python package for providing Mozilla's CA Bundle."
category = "main"
optional = false
python-versions = "*"
[[package]]
name = "chardet"
version = "4.0.0"
description = "Universal encoding detector for Python 2 and 3"
name = "charset-normalizer"
version = "2.0.9"
description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet."
category = "main"
optional = false
python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*"
python-versions = ">=3.5.0"
[package.extras]
unicode_backport = ["unicodedata2"]
[[package]]
name = "idna"
version = "2.10"
version = "3.3"
description = "Internationalized Domain Names in Applications (IDNA)"
category = "main"
optional = false
python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*"
python-versions = ">=3.5"
[[package]]
name = "mypy"
version = "0.812"
description = "Optional static typing for Python"
category = "main"
category = "dev"
optional = false
python-versions = ">=3.5"
@ -62,80 +65,81 @@ dmypy = ["psutil (>=4.0)"]
name = "mypy-extensions"
version = "0.4.3"
description = "Experimental type system extensions for programs checked with the mypy typechecker."
category = "main"
category = "dev"
optional = false
python-versions = "*"
[[package]]
name = "requests"
version = "2.25.1"
version = "2.26.0"
description = "Python HTTP for Humans."
category = "main"
optional = false
python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*"
python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, !=3.5.*"
[package.dependencies]
certifi = ">=2017.4.17"
chardet = ">=3.0.2,<5"
idna = ">=2.5,<3"
charset-normalizer = {version = ">=2.0.0,<2.1.0", markers = "python_version >= \"3\""}
idna = {version = ">=2.5,<4", markers = "python_version >= \"3\""}
urllib3 = ">=1.21.1,<1.27"
[package.extras]
security = ["pyOpenSSL (>=0.14)", "cryptography (>=1.3.4)"]
socks = ["PySocks (>=1.5.6,!=1.5.7)", "win-inet-pton"]
use_chardet_on_py3 = ["chardet (>=3.0.2,<5)"]
[[package]]
name = "typed-ast"
version = "1.4.3"
description = "a fork of Python 2 and 3 ast modules with type comment support"
category = "main"
category = "dev"
optional = false
python-versions = "*"
[[package]]
name = "typing-extensions"
version = "3.10.0.0"
description = "Backported and Experimental Type Hints for Python 3.5+"
category = "main"
version = "4.0.1"
description = "Backported and Experimental Type Hints for Python 3.6+"
category = "dev"
optional = false
python-versions = "*"
python-versions = ">=3.6"
[[package]]
name = "urllib3"
version = "1.22"
version = "1.26.7"
description = "HTTP library with thread-safe connection pooling, file post, and more."
category = "main"
optional = false
python-versions = "*"
python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, <4"
[package.extras]
brotli = ["brotlipy (>=0.6.0)"]
secure = ["pyOpenSSL (>=0.14)", "cryptography (>=1.3.4)", "idna (>=2.0.0)", "certifi", "ipaddress"]
socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"]
[metadata]
lock-version = "1.1"
python-versions = ">=3.7.0"
content-hash = "4fec48a3684b15cd29af1c2f3db5a9033d34a1605ad11aec7babafd2f6bcb1b1"
python-versions = ">=3.7.0,<4"
content-hash = "bee495c33e4a9b337c16d6039644b59138929406641542ed7c8f434e38625811"
[metadata.files]
argo-client = [
{file = "argo-client-0.0.5.tar.gz", hash = "sha256:9b2157f3ea953df812948c27eb762dbe8401bb9d0dc74f49310b6636320a0347"},
{file = "argo_client-0.0.5-py3-none-any.whl", hash = "sha256:745239a231a0d891088ca2aedebd7ec075faf0f19c2f6b0ceafd252e3eed616d"},
{file = "argo-client-0.0.10.tar.gz", hash = "sha256:a95e07201a5e23758e7bc6b2e1d594c61a71df02ff534ad7a8db32fdb991ed0b"},
{file = "argo_client-0.0.10-py3-none-any.whl", hash = "sha256:d86e07bfc421faf9f25be6af2d4a0c7fd2ddef7a759488f6c05baa2ff2c1e390"},
]
bitvector = [
{file = "BitVector-3.5.0.tar.gz", hash = "sha256:cac2fbccf11e325115827ed7be03e5fd62615227b0bbf3fa5a18a842a221839c"},
]
certifi = [
{file = "certifi-2021.5.30-py2.py3-none-any.whl", hash = "sha256:50b1e4f8446b06f41be7dd6338db18e0990601dce795c2b1686458aa7e8fa7d8"},
{file = "certifi-2021.5.30.tar.gz", hash = "sha256:2bbf76fd432960138b3ef6dda3dde0544f27cbf8546c458e60baf371917ba9ee"},
{file = "certifi-2021.10.8-py2.py3-none-any.whl", hash = "sha256:d62a0163eb4c2344ac042ab2bdf75399a71a2d8c7d47eac2e2ee91b9d6339569"},
{file = "certifi-2021.10.8.tar.gz", hash = "sha256:78884e7c1d4b00ce3cea67b44566851c4343c120abd683433ce934a68ea58872"},
]
chardet = [
{file = "chardet-4.0.0-py2.py3-none-any.whl", hash = "sha256:f864054d66fd9118f2e67044ac8981a54775ec5b67aed0441892edb553d21da5"},
{file = "chardet-4.0.0.tar.gz", hash = "sha256:0d6f53a15db4120f2b08c94f11e7d93d2c911ee118b6b30a04ec3ee8310179fa"},
charset-normalizer = [
{file = "charset-normalizer-2.0.9.tar.gz", hash = "sha256:b0b883e8e874edfdece9c28f314e3dd5badf067342e42fb162203335ae61aa2c"},
{file = "charset_normalizer-2.0.9-py3-none-any.whl", hash = "sha256:1eecaa09422db5be9e29d7fc65664e6c33bd06f9ced7838578ba40d58bdf3721"},
]
idna = [
{file = "idna-2.10-py2.py3-none-any.whl", hash = "sha256:b97d804b1e9b523befed77c48dacec60e6dcb0b5391d57af6a65a312a90648c0"},
{file = "idna-2.10.tar.gz", hash = "sha256:b307872f855b18632ce0c21c5e45be78c0ea7ae4c15c828c20788b26921eb3f6"},
{file = "idna-3.3-py3-none-any.whl", hash = "sha256:84d9dd047ffa80596e0f246e2eab0b391788b0503584e8945f2368256d2735ff"},
{file = "idna-3.3.tar.gz", hash = "sha256:9d643ff0a55b762d5cdb124b8eaa99c66322e2157b69160bc32796e824360e6d"},
]
mypy = [
{file = "mypy-0.812-cp35-cp35m-macosx_10_9_x86_64.whl", hash = "sha256:a26f8ec704e5a7423c8824d425086705e381b4f1dfdef6e3a1edab7ba174ec49"},
@ -166,8 +170,8 @@ mypy-extensions = [
{file = "mypy_extensions-0.4.3.tar.gz", hash = "sha256:2d82818f5bb3e369420cb3c4060a7970edba416647068eb4c5343488a6c604a8"},
]
requests = [
{file = "requests-2.25.1-py2.py3-none-any.whl", hash = "sha256:c210084e36a42ae6b9219e00e48287def368a26d03a048ddad7bfee44f75871e"},
{file = "requests-2.25.1.tar.gz", hash = "sha256:27973dd4a904a4f13b263a19c866c13b92a39ed1c964655f025f3f8d3d75b804"},
{file = "requests-2.26.0-py2.py3-none-any.whl", hash = "sha256:6c1246513ecd5ecd4528a0906f910e8f0f9c6b8ec72030dc9fd154dc1a6efd24"},
{file = "requests-2.26.0.tar.gz", hash = "sha256:b8aa58f8cf793ffd8782d3d8cb19e66ef36f7aba4353eec859e74678b01b07a7"},
]
typed-ast = [
{file = "typed_ast-1.4.3-cp35-cp35m-manylinux1_i686.whl", hash = "sha256:2068531575a125b87a41802130fa7e29f26c09a2833fea68d9a40cf33902eba6"},
@ -202,11 +206,10 @@ typed-ast = [
{file = "typed_ast-1.4.3.tar.gz", hash = "sha256:fb1bbeac803adea29cedd70781399c99138358c26d05fcbd23c13016b7f5ec65"},
]
typing-extensions = [
{file = "typing_extensions-3.10.0.0-py2-none-any.whl", hash = "sha256:0ac0f89795dd19de6b97debb0c6af1c70987fd80a2d62d1958f7e56fcc31b497"},
{file = "typing_extensions-3.10.0.0-py3-none-any.whl", hash = "sha256:779383f6086d90c99ae41cf0ff39aac8a7937a9283ce0a414e5dd782f4c94a84"},
{file = "typing_extensions-3.10.0.0.tar.gz", hash = "sha256:50b6f157849174217d0656f99dc82fe932884fb250826c18350e159ec6cdf342"},
{file = "typing_extensions-4.0.1-py3-none-any.whl", hash = "sha256:7f001e5ac290a0c0401508864c7ec868be4e701886d5b573a9528ed3973d9d3b"},
{file = "typing_extensions-4.0.1.tar.gz", hash = "sha256:4ca091dea149f945ec56afb48dae714f21e8692ef22a395223bcd328961b6a0e"},
]
urllib3 = [
{file = "urllib3-1.22-py2.py3-none-any.whl", hash = "sha256:06330f386d6e4b195fbfc736b297f58c5a892e4440e54d294d7004e3a9bbea1b"},
{file = "urllib3-1.22.tar.gz", hash = "sha256:cc44da8e1145637334317feebd728bd869a35285b93cbb4cca2577da7e62db4f"},
{file = "urllib3-1.26.7-py2.py3-none-any.whl", hash = "sha256:c4fdf4019605b6e5423637e01bc9fe4daef873709a7973e195ceba0a62bbc844"},
{file = "urllib3-1.26.7.tar.gz", hash = "sha256:4987c65554f7a2dbf30c18fd48778ef124af6fab771a377103da0585e2336ece"},
]

11
cryptol-remote-api/python/pyproject.toml
View File

@ -1,10 +1,11 @@
[tool.poetry]
name = "cryptol"
version = "2.11.2"
version = "2.12.3"
readme = "README.md"
keywords = ["cryptography", "verification"]
description = "Cryptol client for the Cryptol 2.11 RPC server"
authors = ["Andrew Kent <andrew@galois.com>", "Aaron Tomb <atomb@galois.com>"]
description = "Cryptol client for the Cryptol 2.12 RPC server"
authors = ["Galois, Inc. <cryptol-team@galois.com>"]
license = "BSD License"
include = [
"LICENSE",
@ -12,10 +13,10 @@ include = [
]
[tool.poetry.dependencies]
python = ">=3.7.0"
python = ">=3.7.0,<4"
requests = "^2.25.1"
BitVector = "^3.4.9"
argo-client = "0.0.5"
argo-client = "0.0.10"
[tool.poetry.dev-dependencies]
mypy = "^0.812"

28
cryptol-remote-api/python/tests/cryptol/test-files/Types.cry Normal file
View File

@ -0,0 +1,28 @@
module Types where
b : Bit
b = True
w : [16]
w = 42
z : Integer
z = 420000
m : Z 12
m = 6
q : Rational
q = ratio 5 4
t : (Bit, Integer)
t = (False, 7)
s : [3][3][8]
s = [[1, 2, 3], [4, 5, 6], [7, 8, 9]]
r : {xCoord : [32], yCoord : [32]}
r = {xCoord = 12 : [32], yCoord = 21 : [32]}
id : {n} (fin n) => [n] -> [n]
id a = a

21
cryptol-remote-api/python/tests/cryptol/test_AES.py
View File

@ -2,36 +2,37 @@ import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.single_connection import *
from cryptol.bitvector import BV
class TestAES(unittest.TestCase):
def test_AES(self):
c = cryptol.connect(verify=False)
c.load_file(str(Path('tests','cryptol','test-files', 'examples','AES.cry')))
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files', 'examples','AES.cry')))
pt = BV(size=128, value=0x3243f6a8885a308d313198a2e0370734)
key = BV(size=128, value=0x2b7e151628aed2a6abf7158809cf4f3c)
ct = c.call("aesEncrypt", (pt, key)).result()
ct = call("aesEncrypt", (pt, key))
expected_ct = BV(size=128, value=0x3925841d02dc09fbdc118597196a0b32)
self.assertEqual(ct, expected_ct)
decrypted_ct = c.call("aesDecrypt", (ct, key)).result()
decrypted_ct = call("aesDecrypt", (ct, key))
self.assertEqual(pt, decrypted_ct)
pt = BV(size=128, value=0x00112233445566778899aabbccddeeff)
key = BV(size=128, value=0x000102030405060708090a0b0c0d0e0f)
ct = c.call("aesEncrypt", (pt, key)).result()
ct = call("aesEncrypt", (pt, key))
expected_ct = BV(size=128, value=0x69c4e0d86a7b0430d8cdb78070b4c55a)
self.assertEqual(ct, expected_ct)
decrypted_ct = c.call("aesDecrypt", (ct, key)).result()
decrypted_ct = call("aesDecrypt", (ct, key))
self.assertEqual(pt, decrypted_ct)
self.assertTrue(c.safe("aesEncrypt"))
self.assertTrue(c.safe("aesDecrypt"))
self.assertTrue(c.check("AESCorrect").result().success)
# c.prove("AESCorrect") # probably takes too long for this script...?
self.assertTrue(safe("aesEncrypt"))
self.assertTrue(safe("aesDecrypt"))
self.assertTrue(check("AESCorrect"))
# prove("AESCorrect") # probably takes too long for this script...?

35
cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py
View File

@ -2,30 +2,31 @@ import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.single_connection import *
from cryptol.bitvector import BV
class TestCplxQ(unittest.TestCase):
def test_CplxQ(self):
c = cryptol.connect(reset_server=True, verify=False)
c.load_file(str(Path('tests','cryptol','test-files', 'CplxQNewtype.cry')))
connect(verify=False)
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()
forty_two = cry_eval("fortyTwo")
cplx_forty_two1 = call("embedQ", forty_two)
cplx_forty_two2 = cry_eval("CplxQ{ real = 42, imag = 0 }")
cplx_two = cry_eval("cplxTwo")
cplx_forty = cry_eval("cplxForty")
cplx_forty_two3 = call("cplxAdd", cplx_two, cplx_forty)
cplx_forty_two4 = cry_eval("cplxMul (CplxQ{ real = 21, imag = 0 }) (CplxQ{ real = 2, imag = 0 })")
cplx_forty_two5 = cry_eval("cplxAdd (CplxQ{ real = 41, imag = 0 }) (CplxQ{ real = 1, imag = 0 })")
cplx_forty_two6 = cry_eval("CplxQ{ real = 42, imag = 0 }")
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())
self.assertTrue(call("cplxEq", cplx_forty_two1, cplx_forty_two2))
self.assertFalse(call("cplxEq", cplx_two, cplx_forty_two2))
self.assertTrue(call("cplxEq", cplx_forty_two1, cplx_forty_two3))
self.assertTrue(call("cplxEq", cplx_forty_two1, cplx_forty_two4))
self.assertTrue(call("cplxEq", cplx_forty_two1, cplx_forty_two5))
self.assertTrue(call("cplxEq", cplx_forty_two1, cplx_forty_two6))

24
cryptol-remote-api/python/tests/cryptol/test_DES.py
View File

@ -2,44 +2,44 @@ import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.cryptoltypes import CryptolApplication, CryptolLiteral
from cryptol.single_connection import *
from cryptol.bitvector import BV
class TestDES(unittest.TestCase):
def test_SHA256(self):
c = cryptol.connect(verify=False)
c.load_file(str(Path('tests','cryptol','test-files','examples','DEStest.cry')))
def test_DES(self):
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files','examples','DEStest.cry')))
# we can run the test suite as indended...
# vkres = c.eval('vktest DES').result()
# vkres = cry_eval('vktest DES')
# self.assertTrue(all(passed for (_,_,passed) in vkres))
# vtres = c.eval('vttest DES').result()
# vtres = cry_eval('vttest DES')
# self.assertTrue(all(passed for (_,_,passed) in vtres))
# kares = c.eval('katest DES').result()
# kares = cry_eval('katest DES')
# self.assertTrue(all(passed for (_,_,passed) in kares))
# ...but we can also do it manually, using the python bindings more
def test(key, pt0, ct0):
ct1 = c.call('DES.encrypt', key, pt0).result()
pt1 = c.call('DES.decrypt', key, ct0).result()
ct1 = call('DES.encrypt', key, pt0)
pt1 = call('DES.decrypt', key, ct0)
self.assertEqual(ct0, ct1)
self.assertEqual(pt0, pt1)
# vktest
vk = c.eval('vk').result()
vk = cry_eval('vk')
pt0 = BV(size=64, value=0)
for (key, ct0) in vk:
test(key, pt0, ct0)
# vttest
vt = c.eval('vt').result()
vt = cry_eval('vt')
key = BV(size=64, value=0x0101010101010101)
for (pt0, ct0) in vt:
test(key, pt0, ct0)
# katest
ka = c.eval('ka').result()
ka = cry_eval('ka')
for (key, pt0, ct0) in ka:
test(key, pt0, ct0)

18
cryptol-remote-api/python/tests/cryptol/test_EvenMansour.py
View File

@ -2,24 +2,24 @@ import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.cryptoltypes import CryptolApplication, CryptolLiteral
from cryptol.single_connection import *
from cryptol.bitvector import BV
class TestEvenMansour(unittest.TestCase):
def test_EvenMansour(self):
c = cryptol.connect(verify=False)
c.load_file(str(Path('tests','cryptol','test-files','examples','contrib','EvenMansour.cry')))
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files','examples','contrib','EvenMansour.cry')))
F_10_4 = c.eval('F:[10][4]').result()
self.assertTrue(c.call('is_a_permutation', F_10_4).result())
F_10_4 = cry_eval('F:[10][4]')
self.assertTrue(call('is_a_permutation', F_10_4))
Finv_10_4 = c.eval("F':[10][4]").result()
Finv_10_4 = cry_eval("F':[10][4]")
digits = [ BV(size=4, value=i) for i in range(0,10) ]
# ^ the same as: c.eval('[0..9]:[_][4]').result()
self.assertTrue(c.call('is_inverse_permutation', digits, F_10_4, Finv_10_4).result())
# ^ the same as: c.eval('[0..9]:[_][4]')
self.assertTrue(call('is_inverse_permutation', digits, F_10_4, Finv_10_4))
self.assertTrue(c.check('E_and_D_are_inverses').result().success)
self.assertTrue(check('E_and_D_are_inverses'))
if __name__ == "__main__":

19
cryptol-remote-api/python/tests/cryptol/test_SHA256.py
View File

@ -2,30 +2,31 @@ import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.cryptoltypes import CryptolApplication, CryptolLiteral
from cryptol.single_connection import *
from cryptol.cryptoltypes import CryptolLiteral
from cryptol.bitvector import BV
class TestSHA256(unittest.TestCase):
def test_SHA256(self):
c = cryptol.connect(verify=False)
c.load_file(str(Path('tests','cryptol','test-files','examples','param_modules','SHA.cry')))
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files','examples','param_modules','SHA.cry')))
m1 = CryptolLiteral('"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"')
j1 = c.call('join', m1).result()
h1 = c.call('sha256', j1).result()
j1 = call('join', m1)
h1 = call('sha256', j1)
expected_h1 = BV(size=256, value=0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1)
self.assertEqual(h1, expected_h1)
m2 = CryptolLiteral('""')
j2 = c.call('join', m2).result()
h2 = c.call('sha256', j2).result()
j2 = call('join', m2)
h2 = call('sha256', j2)
expected_h2 = BV(size=256, value=0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855)
self.assertEqual(h2, expected_h2)
m3 = CryptolLiteral('"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"')
j3 = c.call('join', m3).result()
h3 = c.call('sha256', j3).result()
j3 = call('join', m3)
h3 = call('sha256', j3)
expected_h3 = BV(size=256, value=0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1)
self.assertEqual(h3, expected_h3)

183
cryptol-remote-api/python/tests/cryptol/test_basics.py
View File

@ -1,16 +1,14 @@
import unittest
from argo_client.interaction import ArgoException
from pathlib import Path
import unittest
import io
import os
from pathlib import Path
import subprocess
import time
import unittest
import signal
from distutils.spawn import find_executable
import cryptol
import argo_client.connection as argo
import cryptol.cryptoltypes
from cryptol import solver
from cryptol.single_connection import *
from cryptol.bitvector import BV
from BitVector import * #type: ignore
@ -19,27 +17,178 @@ from BitVector import * #type: ignore
# focused on intricate Cryptol specifics per se.
class BasicServerTests(unittest.TestCase):
# Connection to cryptol
c = None
@classmethod
def setUpClass(self):
self.c = cryptol.connect(verify=False)
@classmethod
def tearDownClass(self):
if self.c:
self.c.reset()
def test_extend_search_path(self):
"""Test that extending the search path acts as expected w.r.t. loads."""
# Test that extending the search path acts as expected w.r.t. loads
c = self.c
c.extend_search_path(str(Path('tests','cryptol','test-files', 'test-subdir')))
c.load_module('Bar')
ans1 = c.evaluate_expression("theAnswer").result()
ans2 = c.evaluate_expression("id theAnswer").result()
c.load_module('Bar').result()
ans1 = c.eval("theAnswer").result()
ans2 = c.eval("id theAnswer").result()
self.assertEqual(ans1, ans2)
def test_logging(self):
c = self.c
c.extend_search_path(str(Path('tests','cryptol','test-files', 'test-subdir')))
c.load_module('Bar').result()
log_buffer = io.StringIO()
c.logging(on=True, dest=log_buffer)
_ = c.eval("theAnswer").result()
contents = log_buffer.getvalue()
self.assertEqual(len(contents.strip().splitlines()), 2,
msg=f'log contents: {str(contents.strip().splitlines())}')
_ = c.eval("theAnswer").result()
def test_check_timeout(self):
c = self.c
c.load_file(str(Path('tests','cryptol','test-files', 'examples','AES.cry'))).result()
t1 = time.time()
with self.assertRaises(ArgoException):
c.check("\\(bv : [256]) -> ~ (~ (~ (~bv))) == bv", num_tests="all", timeout=1.0).result()
t2 = time.time()
self.assertLess(t2 - t1, 2.0)
t1 = time.time()
with self.assertRaises(ArgoException):
c.check("\\(bv : [256]) -> ~ (~ (~ (~bv))) == bv", num_tests="all", timeout=5.0).result()
t2 = time.time()
self.assertLess(t2 - t1, 7)
t1 = time.time()
c.check("\\(bv : [256]) -> ~ (~ (~ (~bv))) == bv", num_tests=10, timeout=5.0).result()
t2 = time.time()
self.assertLess(t2 - t1, 5)
def test_interrupt(self):
# Check if this test is using a local server, if not we assume it's a remote HTTP server
if os.getenv('CRYPTOL_SERVER') is not None or find_executable('cryptol-remote-api'):
c = self.c
c.load_file(str(Path('tests','cryptol','test-files', 'examples','AES.cry')))
t1 = time.time()
c.check("\\(bv : [256]) -> ~ (~ (~ (~bv))) == bv", num_tests="all", timeout=30.0)
# ^ .result() intentionally omitted so we don't wait on it's result and we can interrupt
# it on the next line. We add a timeout just in case to the test fails
time.sleep(.5)
c.interrupt()
self.assertTrue(c.safe("aesEncrypt").result())
t2 = time.time()
self.assertLess(t2 - t1, 15.0) # ensure th interrupt ended things and not the timeout
elif os.getenv('CRYPTOL_SERVER_URL') is not None:
c = self.c
other_c = cryptol.connect(verify=False)
# Since this is the HTTP server, due to client implementation details
# the requests don't return until they get a response, so we fork
# to interrupt the server
newpid = os.fork()
if newpid == 0:
time.sleep(5)
other_c.interrupt()
os._exit(0)
c.load_file(str(Path('tests','cryptol','test-files', 'examples','AES.cry')))
t1 = time.time()
c.check("\\(bv : [256]) -> ~ (~ (~ (~bv))) == bv", num_tests="all", timeout=60.0)
self.assertTrue(c.safe("aesEncrypt").result())
t2 = time.time()
self.assertLess(t2 - t1, 20.0) # ensure th interrupt ended things and not the timeout
else:
# Otherwise fail... since this shouldn't be possible
self.assertFalse("Impossible")
def test_prove_timeout(self):
c = self.c
c.load_file(str(Path('tests','cryptol','test-files', 'examples','AES.cry')))
pt = BV(size=128, value=0x3243f6a8885a308d313198a2e0370734)
key = BV(size=128, value=0x2b7e151628aed2a6abf7158809cf4f3c)
ct = c.call("aesEncrypt", (pt, key)).result()
expected_ct = BV(size=128, value=0x3925841d02dc09fbdc118597196a0b32)
self.assertEqual(ct, expected_ct)
decrypted_ct = c.call("aesDecrypt", (ct, key)).result()
self.assertEqual(pt, decrypted_ct)
pt = BV(size=128, value=0x00112233445566778899aabbccddeeff)
key = BV(size=128, value=0x000102030405060708090a0b0c0d0e0f)
ct = c.call("aesEncrypt", (pt, key)).result()
expected_ct = BV(size=128, value=0x69c4e0d86a7b0430d8cdb78070b4c55a)
self.assertEqual(ct, expected_ct)
decrypted_ct = c.call("aesDecrypt", (ct, key)).result()
self.assertEqual(pt, decrypted_ct)
self.assertTrue(c.safe("aesEncrypt").result())
self.assertTrue(c.safe("aesDecrypt").result())
self.assertTrue(c.check("AESCorrect").result().success)
t1 = time.time()
with self.assertRaises(ArgoException):
c.prove("AESCorrect", timeout=1.0).result()
t2 = time.time()
# check the timeout worked
self.assertGreaterEqual(t2 - t1, 1.0)
self.assertLess(t2 - t1, 5.0)
# make sure things are still working
self.assertTrue(c.safe("aesEncrypt").result())
# set the timeout at the connection level
c.timeout = 1.0
t1 = time.time()
with self.assertRaises(ArgoException):
c.prove("AESCorrect").result()
t2 = time.time()
# check the timeout worked
self.assertGreaterEqual(t2 - t1, 1.0)
self.assertLess(t2 - t1, 5.0)
# make sure things are still working
c.timeout = None
self.assertTrue(c.safe("aesEncrypt").result())
c.timeout = 1.0
t1 = time.time()
with self.assertRaises(ArgoException):
# override timeout with longer time
c.prove("AESCorrect", timeout=5.0).result()
t2 = time.time()
self.assertGreaterEqual(t2 - t1, 5.0)
self.assertLess(t2 - t1, 10.0)
# make sure things are still working
c.timeout = None
self.assertTrue(c.safe("aesEncrypt").result())
class BasicLoggingServerTests(unittest.TestCase):
# Connection to cryptol
log_buffer = None
@classmethod
def setUpClass(self):
self.log_buffer = io.StringIO()
connect(verify=False, log_dest = self.log_buffer)
def test_logging(self):
extend_search_path(str(Path('tests','cryptol','test-files', 'test-subdir')))
load_module('Bar')
_ = cry_eval("theAnswer")
content_lines = self.log_buffer.getvalue().strip().splitlines()
self.assertEqual(len(content_lines), 6,
msg=f'log contents: {str(content_lines)}')
if __name__ == "__main__":
unittest.main()

151
cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py
View File

@ -10,39 +10,32 @@ from distutils.spawn import find_executable
import cryptol
import argo_client.connection as argo
import cryptol.cryptoltypes
from cryptol.single_connection import *
from cryptol import solver
from cryptol.bitvector import BV
from BitVector import * #type: ignore
class CryptolTests(unittest.TestCase):
# Connection to cryptol
c = None
@classmethod
def setUpClass(self):
self.c = cryptol.connect(verify=False)
self.c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
@classmethod
def tearDownClass(self):
if self.c:
self.c.reset()
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
def test_low_level(self):
c = self.c
x_val = c.evaluate_expression("x").result()
x_val = cry_eval("x")
self.assertEqual(c.eval("Id::id x").result(), x_val)
self.assertEqual(c.call('Id::id', bytes.fromhex('ff')).result(), BV(8,255))
self.assertEqual(cry_eval("Id::id x"), x_val)
self.assertEqual(call('Id::id', bytes.fromhex('ff')), BV(8,255))
self.assertEqual(c.call('add', b'\0', b'\1').result(), BV(8,1))
self.assertEqual(c.call('add', bytes.fromhex('ff'), bytes.fromhex('03')).result(), BV(8,2))
self.assertEqual(call('add', b'\0', b'\1'), BV(8,1))
self.assertEqual(call('add', bytes.fromhex('ff'), bytes.fromhex('03')), BV(8,2))
# AMK: importing cryptol bindings into Python temporarily broken due to linear state usage changes
# in argo approx 1 March 2020
# def test_module_import(self):
# c = self.c
# c = cryptol.connect()
# cryptol.add_cryptol_module('Foo', c)
# from Foo import add
# self.assertEqual(add(b'\2', 2), BV(8,4))
@ -55,123 +48,131 @@ class CryptolTests(unittest.TestCase):
# self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0))
def test_sat_and_prove(self):
c = self.c
# test a single sat model can be returned
rootsOf9 = c.sat('isSqrtOf9').result()
self.assertEqual(len(rootsOf9), 1)
self.assertTrue(int(rootsOf9[0]) ** 2 % 256, 9)
rootsOf9 = sat('isSqrtOf9')
self.assertTrue(rootsOf9)
self.assertEqual(len(rootsOf9.models), 1)
self.assertEqual(len(rootsOf9.models[0]), 1)
self.assertTrue(int(rootsOf9.models[0][0]) ** 2 % 256, 9)
# check we can specify the solver
rootsOf9 = c.sat('isSqrtOf9', solver = solver.ANY).result()
self.assertEqual(len(rootsOf9), 1)
self.assertTrue(int(rootsOf9[0]) ** 2 % 256, 9)
rootsOf9 = sat('isSqrtOf9', solver = solver.ANY)
self.assertTrue(rootsOf9)
self.assertEqual(len(rootsOf9.models), 1)
self.assertEqual(len(rootsOf9.models[0]), 1)
self.assertTrue(int(rootsOf9.models[0][0]) ** 2 % 256, 9)
# check we can ask for a specific number of results
rootsOf9 = c.sat('isSqrtOf9', count = 3).result()
self.assertEqual(len(rootsOf9), 3)
self.assertEqual([int(root) ** 2 % 256 for root in rootsOf9], [9,9,9])
rootsOf9 = sat('isSqrtOf9', count = 3)
self.assertTrue(rootsOf9)
self.assertEqual(len(rootsOf9.models), 3)
for model in rootsOf9.models:
self.assertEqual(len(model), 1)
self.assertTrue(int(model[0]) ** 2 % 256, 9)
# check we can ask for all results
rootsOf9 = c.sat('isSqrtOf9', count = None).result()
self.assertEqual(len(rootsOf9), 4)
self.assertEqual([int(root) ** 2 % 256 for root in rootsOf9], [9,9,9,9])
rootsOf9 = sat('isSqrtOf9', count = None)
self.assertTrue(rootsOf9)
self.assertEqual(len(rootsOf9.models), 4)
for model in rootsOf9.models:
self.assertEqual(len(model), 1)
self.assertTrue(int(model[0]) ** 2 % 256, 9)
# check for an unsat condition
self.assertFalse(c.sat('\\x -> isSqrtOf9 x && ~(elem x [3,131,125,253])').result())
self.assertFalse(sat('\\x -> isSqrtOf9 x && ~(elem x [3,131,125,253])'))
# check for a valid condition
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]').result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.Z3).result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3).result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3.without_hash_consing()).result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.SBV_Z3).result())
self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.OFFLINE).result(), solver.OfflineSmtQuery)
self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.SBV_OFFLINE).result(), solver.OfflineSmtQuery)
self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.W4_OFFLINE).result(), solver.OfflineSmtQuery)
self.assertTrue(prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]'))
self.assertTrue(prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.Z3))
self.assertTrue(prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3))
self.assertTrue(prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3.without_hash_consing()))
self.assertTrue(prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.SBV_Z3))
self.assertIsInstance(prove('\\(x : [8]) -> x == reverse (reverse x)', solver.OFFLINE), solver.OfflineSmtQuery)
self.assertIsInstance(prove('\\(x : [8]) -> x == reverse (reverse x)', solver.SBV_OFFLINE), solver.OfflineSmtQuery)
self.assertIsInstance(prove('\\(x : [8]) -> x == reverse (reverse x)', solver.W4_OFFLINE), solver.OfflineSmtQuery)
def test_check(self):
c = self.c
res = c.check("\\x -> x==(x:[8])").result()
res = check("\\x -> x==(x:[8])")
self.assertTrue(res.success)
self.assertEqual(res.tests_run, 100)
self.assertEqual(res.tests_possible, 256)
self.assertFalse(len(res.args), 0)
self.assertEqual(res.error_msg, None)
res = c.check("\\x -> x==(x:[8])", num_tests=1).result()
res = check("\\x -> x==(x:[8])", num_tests=1)
self.assertTrue(res.success)
self.assertEqual(res.tests_run, 1)
self.assertEqual(res.tests_possible, 256)
self.assertEqual(len(res.args), 0)
self.assertEqual(res.error_msg, None)
res = c.check("\\x -> x==(x:[8])", num_tests=42).result()
res = check("\\x -> x==(x:[8])", num_tests=42)
self.assertTrue(res.success)
self.assertEqual(res.tests_run, 42)
self.assertEqual(res.tests_possible, 256)
self.assertEqual(len(res.args), 0)
self.assertEqual(res.error_msg, None)
res = c.check("\\x -> x==(x:[8])", num_tests=1000).result()
res = check("\\x -> x==(x:[8])", num_tests=1000)
self.assertTrue(res.success)
self.assertEqual(res.tests_run, 256)
self.assertEqual(res.tests_possible, 256)
self.assertEqual(len(res.args), 0)
self.assertEqual(res.error_msg, None)
res = c.check("\\x -> x==(x:[8])", num_tests='all').result()
res = check("\\x -> x==(x:[8])", num_tests='all')
self.assertTrue(res.success)
self.assertEqual(res.tests_run, 256)
self.assertEqual(res.tests_possible, 256)
self.assertEqual(len(res.args), 0)
self.assertEqual(res.error_msg, None)
res = c.check("\\x -> x==(x:Integer)", num_tests=1024).result()
res = check("\\x -> x==(x:Integer)", num_tests=1024)
self.assertTrue(res.success)
self.assertEqual(res.tests_run, 1024)
self.assertEqual(res.tests_possible, None)
self.assertEqual(len(res.args), 0)
self.assertEqual(res.error_msg, None)
res = c.check("\\x -> (x + 1)==(x:[8])").result()
res = check("\\x -> (x + 1)==(x:[8])")
self.assertFalse(res.success)
self.assertEqual(res.tests_possible, 256)
self.assertEqual(len(res.args), 1)
self.assertEqual(res.error_msg, None)
res = c.check("\\x -> (x / 0)==(x:[8])").result()
res = check("\\x -> (x / 0)==(x:[8])")
self.assertFalse(res.success)
self.assertEqual(res.tests_possible, 256)
self.assertEqual(len(res.args), 1)
self.assertIsInstance(res.error_msg, str)
def test_safe(self):
c = self.c
res = c.safe("\\x -> x==(x:[8])").result()
res = safe("\\x -> x==(x:[8])")
self.assertTrue(res)
res = c.safe("\\x -> x / (x:[8])").result()
self.assertEqual(res, [BV(size=8, value=0)])
res = safe("\\x -> x / (x:[8])")
self.assertFalse(res)
self.assertEqual(res.assignments, [BV(size=8, value=0)])
res = c.safe("\\x -> x / (x:[8])", solver.Z3).result()
self.assertEqual(res, [BV(size=8, value=0)])
res = safe("\\x -> x / (x:[8])", solver.Z3)
self.assertFalse(res)
self.assertEqual(res.assignments, [BV(size=8, value=0)])
res = c.safe("\\x -> x / (x:[8])", solver.W4_Z3).result()
self.assertEqual(res, [BV(size=8, value=0)])
res = safe("\\x -> x / (x:[8])", solver.W4_Z3)
self.assertFalse(res)
self.assertEqual(res.assignments, [BV(size=8, value=0)])
def test_many_usages_one_connection(self):
c = self.c
for i in range(0,100):
x_val1 = c.evaluate_expression("x").result()
x_val2 = c.eval("Id::id x").result()
x_val1 = cry_eval("x")
x_val2 = cry_eval("Id::id x")
self.assertEqual(x_val1, x_val2)
class HttpMultiConnectionTests(unittest.TestCase):
# Connection to server
c = None
# Python initiated process running the server (if any)
p = None
# url of HTTP server
@ -216,26 +217,24 @@ class HttpMultiConnectionTests(unittest.TestCase):
def test_reset_with_many_usages_many_connections(self):
for i in range(0,100):
time.sleep(.05)
c = cryptol.connect(url=self.url, verify=False)
c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
x_val1 = c.evaluate_expression("x").result()
x_val2 = c.eval("Id::id x").result()
connect(url=self.url, verify=False)
load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
x_val1 = cry_eval("x")
x_val2 = cry_eval("Id::id x")
self.assertEqual(x_val1, x_val2)
c.reset()
reset()
def test_reset_server_with_many_usages_many_connections(self):
def test_server_with_many_usages_many_connections(self):
for i in range(0,100):
time.sleep(.05)
c = cryptol.connect(url=self.url, reset_server=True, verify=False)
c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
x_val1 = c.evaluate_expression("x").result()
x_val2 = c.eval("Id::id x").result()
connect(url=self.url, verify=False)
load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
x_val1 = cry_eval("x")
x_val2 = cry_eval("Id::id x")
self.assertEqual(x_val1, x_val2)
class TLSConnectionTests(unittest.TestCase):
# Connection to server
c = None
# Python initiated process running the server (if any)
p = None
# url of HTTP server
@ -281,10 +280,10 @@ class TLSConnectionTests(unittest.TestCase):
def test_tls_connection(self):
if self.run_tests:
c = cryptol.connect(url=self.url, verify=False)
c.load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
x_val1 = c.evaluate_expression("x").result()
x_val2 = c.eval("Id::id x").result()
connect(url=self.url, verify=False)
load_file(str(Path('tests','cryptol','test-files', 'Foo.cry')))
x_val1 = cry_eval("x")
x_val2 = cry_eval("Id::id x")
self.assertEqual(x_val1, x_val2)
if __name__ == "__main__":

32
cryptol-remote-api/python/tests/cryptol/test_error_recovery.py Normal file
View File

@ -0,0 +1,32 @@
import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.single_connection import *
from argo_client.interaction import ArgoException
from cryptol.bitvector import BV
class TestErrorRecovery(unittest.TestCase):
def test_ErrorRecovery(self):
connect(verify=False)
with self.assertRaises(ArgoException):
load_file(str(Path('tests','cryptol','test-files','bad.cry')))
# test that loading a valid file still works after an exception
load_file(str(Path('tests','cryptol','test-files','Foo.cry')))
# ensure that we really did load the file with no errors
x_val1 = cry_eval("x")
x_val2 = cry_eval("Id::id x")
self.assertEqual(x_val1, x_val2)
# test that a reset still works after an exception (this used to throw
# an error before the server even had a chance to respond because of
# the `connection.protocol_state()` call in `CryptolReset`)
reset()
if __name__ == "__main__":
unittest.main()

48
cryptol-remote-api/python/tests/cryptol/test_quoting.py Normal file
View File

@ -0,0 +1,48 @@
import unittest
from pathlib import Path
import unittest
import cryptol
from cryptol.single_connection import *
from cryptol.bitvector import BV
from cryptol.quoting import *
class TestQuoting(unittest.TestCase):
def test_quoting(self):
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files', 'M.cry')))
x = BV(size=8, value=1)
y = cry_f('g {x}')
z = cry_f('h {y}')
self.assertEqual(z, cry('h (g 0x01)'))
self.assertEqual(cry_eval(z), [x,x])
y = cry_eval_f('g {x}')
z = cry_eval_f('h {y}')
self.assertEqual(y, [x,x])
self.assertEqual(z, [x,x])
self.assertEqual(cry_f('id {BV(size=7, value=1)}'), cry('id (1 : [7])'))
self.assertEqual(cry_eval_f('id {BV(size=7, value=1)}'), BV(size=7, value=1))
self.assertEqual(cry_f('{ {"a": x, "b": x} }'), cry('{a = 0x01, b = 0x01}'))
self.assertEqual(cry_f('{{a = {x}, b = {x}}}'), cry('{a = 0x01, b = 0x01}'))
self.assertEqual(cry_f('id {5}'), cry('id 5'))
self.assertEqual(cry_f('id {5!s}'), cry('id "5"'))
self.assertEqual(cry_f('id {5:#x}'), cry('id "0x5"'))
self.assertEqual(cry_f('id {BV(4,5)}'), cry('id 0x5'))
# Only here to check backwards compatability, the above syntax is preferred
y = cry('g')(cry_f('{x}'))
z = cry('h')(cry_f('{y}'))
self.assertEqual(str(z), str(cry('(h) ((g) (0x01))')))
self.assertEqual(cry_eval(z), [x,x])
self.assertEqual(str(cry('id')(cry_f('{BV(size=7, value=1)}'))), str(cry('(id) (1 : [7])')))
# This is why this syntax is not preferred
with self.assertRaises(ValueError):
cry('g')(x) # x is not CryptolJSON
if __name__ == "__main__":
unittest.main()

86
cryptol-remote-api/python/tests/cryptol/test_smt.py Normal file
View File

@ -0,0 +1,86 @@
import unittest
from pathlib import Path
import unittest
import cryptol
import cryptol.solver as solver
from cryptol.single_connection import *
from cryptol.bitvector import BV
class TestSMT(unittest.TestCase):
def test_SMT(self):
connect(verify=False)
load_module('Cryptol')
ex_true = '\(x : [8]) -> x+x == x+x'
ex_true_safe = safe(ex_true)
self.assertTrue(ex_true_safe)
self.assertIsInstance(ex_true_safe, cryptol.Safe)
ex_true_prove = prove(ex_true)
self.assertTrue(ex_true_prove)
self.assertIsInstance(ex_true_prove, cryptol.Qed)
ex_true_sat = sat(ex_true)
self.assertTrue(ex_true_sat)
self.assertIsInstance(ex_true_sat, cryptol.Satisfiable)
ex_false = '\(x : [8]) -> x+2*x+1 == x'
ex_false_safe = safe(ex_false)
self.assertTrue(ex_false_safe)
self.assertIsInstance(ex_false_safe, cryptol.Safe)
ex_false_prove = prove(ex_false)
self.assertFalse(ex_false_prove)
self.assertIsInstance(ex_false_prove, cryptol.Counterexample)
self.assertEqual(ex_false_prove.type, "predicate falsified")
ex_false_sat = sat(ex_false)
self.assertFalse(ex_false_sat)
self.assertIsInstance(ex_false_sat, cryptol.Unsatisfiable)
ex_partial = '\(x : [8]) -> if x < 0x0f then x == x else error "!"'
ex_partial_safe = safe(ex_partial)
self.assertFalse(ex_partial_safe)
self.assertIsInstance(ex_partial_safe, cryptol.Counterexample)
self.assertEqual(ex_partial_safe.type, "safety violation")
ex_partial_prove = prove(ex_partial)
self.assertFalse(ex_partial_prove)
self.assertIsInstance(ex_partial_prove, cryptol.Counterexample)
self.assertEqual(ex_partial_prove.type, "safety violation")
ex_partial_sat = sat(ex_partial)
self.assertTrue(ex_partial_sat)
self.assertIsInstance(ex_partial_sat, cryptol.Satisfiable)
def test_each_online_solver(self):
# We test each solver that is packaged for use with what4
# via https://github.com/GaloisInc/what4-solvers - the others
# are commented out for now.
ex_true = '\(x : [128]) -> negate (complement x + 1) == complement (negate x) + 1'
solvers = \
[solver.CVC4,
solver.YICES,
solver.Z3,
#solver.BOOLECTOR,
#solver.MATHSAT,
solver.ABC,
#solver.OFFLINE,
solver.ANY,
solver.SBV_CVC4,
solver.SBV_YICES,
solver.SBV_Z3,
#solver.SBV_BOOLECTOR,
#solver.SBV_MATHSAT,
solver.SBV_ABC,
#solver.SBV_OFFLINE,
solver.SBV_ANY,
solver.W4_CVC4,
solver.W4_YICES,
solver.W4_Z3,
#solver.W4_BOOLECTOR,
#solver.W4_OFFLINE,
solver.W4_ABC,
solver.W4_ANY]
for s in solvers:
self.assertTrue(prove(ex_true, s))
if __name__ == "__main__":
unittest.main()

74
cryptol-remote-api/python/tests/cryptol/test_types.py Normal file
View File

@ -0,0 +1,74 @@
import unittest
from argo_client.interaction import ArgoException
from pathlib import Path
import unittest
import cryptol
from cryptol.single_connection import *
from cryptol.opaque import OpaqueValue
from cryptol.bitvector import BV
from cryptol import cryptoltypes
class CryptolTypeTests(unittest.TestCase):
def test_types(self):
connect(verify=False)
load_file(str(Path('tests','cryptol','test-files','Types.cry')))
# Bits
self.assertEqual(cry_eval('b'), True)
self.assertEqual(check_type('b'), cryptoltypes.Bit())
# Words
self.assertEqual(cry_eval('w'), BV(size=16, value=42))
self.assertEqual(check_type('w'), cryptoltypes.Bitvector(cryptoltypes.Num(16)))
# Integers
self.assertEqual(cry_eval('z'), 420000)
self.assertEqual(check_type('z'), cryptoltypes.Integer())
# Modular integers - not supported as values
with self.assertRaises(ValueError):
cry_eval('m')
self.assertEqual(check_type('m'), cryptoltypes.Z(cryptoltypes.Num(12)))
# Rationals - supported only as opaque values
self.assertIsInstance(cry_eval('q'), OpaqueValue)
self.assertEqual(check_type('q'), cryptoltypes.Rational())
# Tuples
self.assertEqual(cry_eval('t'), (False, 7))
t_ty = cryptoltypes.Tuple(cryptoltypes.Bit(), cryptoltypes.Integer())
self.assertEqual(check_type('t'), t_ty)
# Sequences
self.assertEqual(cry_eval('s'),
[[BV(size=8, value=1), BV(size=8, value=2), BV(size=8, value=3)],
[BV(size=8, value=4), BV(size=8, value=5), BV(size=8, value=6)],
[BV(size=8, value=7), BV(size=8, value=8), BV(size=8, value=9)]])
s_ty = cryptoltypes.Sequence(cryptoltypes.Num(3),
cryptoltypes.Sequence(cryptoltypes.Num(3),
cryptoltypes.Bitvector(cryptoltypes.Num(8))))
self.assertEqual(check_type('s'), s_ty)
# Records
self.assertEqual(cry_eval('r'),
{'xCoord': BV(size=32, value=12),
'yCoord': BV(size=32, value=21)})
r_ty = cryptoltypes.Record({
'xCoord': cryptoltypes.Bitvector(cryptoltypes.Num(32)),
'yCoord': cryptoltypes.Bitvector(cryptoltypes.Num(32))})
self.assertEqual(check_type('r'), r_ty)
# Functions - not supported as values
with self.assertRaises(ArgoException):
cry_eval('id')
n = cryptoltypes.Var('n', 'Num')
id_ty = cryptoltypes.CryptolTypeSchema(
{n.name: n.kind}, [cryptoltypes.PropCon('fin', n)],
cryptoltypes.Function(cryptoltypes.Bitvector(n),
cryptoltypes.Bitvector(n)))
self.assertEqual(check_type('id'), id_ty)
if __name__ == "__main__":
unittest.main()

4
cryptol-remote-api/python/tests/cryptol_eval/test_basics.py
View File

@ -102,10 +102,10 @@ class HttpMultiConnectionTests(unittest.TestCase):
self.assertEqual(res, [BV(size=8,value=0xff), BV(size=8,value=0xff)])
c.reset()
def test_reset_server_with_many_usages_many_connections(self):
def test_server_with_many_usages_many_connections(self):
for i in range(0,100):
time.sleep(.05)
c = cryptol.connect(url=self.url, reset_server=True)
c = cryptol.connect(url=self.url)
res = c.call('f', BV(size=8,value=0xff)).result()
self.assertEqual(res, [BV(size=8,value=0xff), BV(size=8,value=0xff)])

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

@ -23,6 +23,7 @@ get_server() {
}
echo "Setting up python environment for remote server clients..."
poetry update
poetry install
echo "Typechecking code with mypy..."
@ -30,10 +31,10 @@ run_test poetry run mypy cryptol/ tests/
get_server cryptol-remote-api
echo "Running cryptol-remote-api tests..."
run_test poetry run python -m unittest discover tests/cryptol
run_test poetry run python -m unittest discover --verbose tests/cryptol
get_server cryptol-eval-server
echo "Running cryptol-eval-server tests..."
run_test poetry run python -m unittest discover tests/cryptol_eval
run_test poetry run python -m unittest discover --verbose tests/cryptol_eval
popd

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

@ -85,6 +85,9 @@ modifyModuleEnv f =
getTCSolver :: CryptolCommand SMT.Solver
getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
getTCSolverConfig :: CryptolCommand SMT.SolverConfig
getTCSolverConfig = CryptolCommand $ const $ solverConfig <$> Argo.getState
liftModuleCmd :: ModuleCmd a -> CryptolCommand a
liftModuleCmd cmd =
do Options callStacks evOpts <- getOptions
@ -123,6 +126,7 @@ data ServerState =
ServerState { _loadedModule :: Maybe LoadedModule
, _moduleEnv :: ModuleEnv
, _tcSolver :: SMT.Solver
, solverConfig :: SMT.SolverConfig
}
loadedModule :: Lens' ServerState (Maybe LoadedModule)
@ -138,14 +142,24 @@ tcSolver = lens _tcSolver (\v n -> v { _tcSolver = n })
initialState :: IO ServerState
initialState =
do modEnv <- initialModuleEnv
s <- SMT.startSolver (defaultSolverConfig (meSearchPath modEnv))
pure (ServerState Nothing modEnv s)
-- NOTE: the "pure ()" is a callback which is invoked if/when the solver
-- stops for some reason. This is just a placeholder for now, and could
-- be replaced by something more useful.
let sCfg = defaultSolverConfig (meSearchPath modEnv)
s <- SMT.startSolver (pure ()) sCfg
pure (ServerState Nothing modEnv s sCfg)
extendSearchPath :: [FilePath] -> ServerState -> ServerState
extendSearchPath paths =
over moduleEnv $ \me -> me { meSearchPath = nubOrd $ paths ++ meSearchPath me }
resetTCSolver :: CryptolCommand ()
resetTCSolver = do
s <- getTCSolver
sCfg <- getTCSolverConfig
liftIO $ SMT.resetSolver s sCfg
instance FreshM CryptolCommand where
liftSupply f = do
serverState <- CryptolCommand $ const Argo.getState

68
cryptol-remote-api/src/CryptolServer/AesonCompat.hs Normal file
View File

@ -0,0 +1,68 @@
{-# LANGUAGE CPP #-}
-- | A compatibility shim for papering over the differences between
-- @aeson-2.0.*@ and pre-2.0.* versions of @aeson@.
--
-- TODO: When the ecosystem widely uses @aeson-2.0.0.0@ or later, remove this
-- module entirely.
module CryptolServer.AesonCompat where
import Data.HashMap.Strict (HashMap)
import Data.Text (Text)
#if MIN_VERSION_aeson(2,0,0)
import Data.Aeson.Key (Key)
import qualified Data.Aeson.Key as K
import Data.Aeson.KeyMap (KeyMap)
import qualified Data.Aeson.KeyMap as KM
#else
import qualified Data.HashMap.Strict as HM
#endif
#if MIN_VERSION_aeson(2,0,0)
type KeyCompat = Key
deleteKM :: Key -> KeyMap v -> KeyMap v
deleteKM = KM.delete
fromListKM :: [(Key, v)] -> KeyMap v
fromListKM = KM.fromList
keyFromText :: Text -> Key
keyFromText = K.fromText
keyToText :: Key -> Text
keyToText = K.toText
lookupKM :: Key -> KeyMap v -> Maybe v
lookupKM = KM.lookup
toHashMapTextKM :: KeyMap v -> HashMap Text v
toHashMapTextKM = KM.toHashMapText
toListKM :: KeyMap v -> [(Key, v)]
toListKM = KM.toList
#else
type KeyCompat = Text
deleteKM :: Text -> HashMap Text v -> HashMap Text v
deleteKM = HM.delete
fromListKM :: [(Text, v)] -> HashMap Text v
fromListKM = HM.fromList
keyFromText :: Text -> Text
keyFromText = id
keyToText :: Text -> Text
keyToText = id
lookupKM :: Text -> HashMap Text v -> Maybe v
lookupKM = HM.lookup
toHashMapTextKM :: HashMap Text v -> HashMap Text v
toHashMapTextKM = id
toListKM :: HashMap Text v -> [(Text, v)]
toListKM = HM.toList
#endif

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

@ -39,6 +39,7 @@ import CryptolServer
liftModuleCmd,
CryptolMethod(raise),
CryptolCommand )
import CryptolServer.AesonCompat (KeyCompat)
import CryptolServer.Exceptions (evalPolyErr)
import CryptolServer.Data.Expression
( readBack, getExpr, Expression)
@ -118,7 +119,7 @@ data CheckResult =
, checkTestsPossible :: Maybe Integer
}
convertServerTestResult :: ServerTestResult -> [(Text, JSON.Value)]
convertServerTestResult :: ServerTestResult -> [(KeyCompat, JSON.Value)]
convertServerTestResult Pass = ["result" .= ("pass" :: Text)]
convertServerTestResult (FailFalse args) =
[ "result" .= ("fail" :: Text)

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

@ -60,6 +60,7 @@ import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)
import Argo
import qualified Argo.Doc as Doc
import CryptolServer
import CryptolServer.AesonCompat
import CryptolServer.Exceptions
import CryptolServer.Data.Type
@ -160,9 +161,9 @@ instance JSON.FromJSON TypeArguments where
parseJSON =
withObject "type arguments" $ \o ->
TypeArguments . Map.fromList <$>
traverse elt (HM.toList o)
traverse elt (toListKM o)
where
elt (name, ty) = (mkIdent name,) <$> parseJSON ty
elt (name, ty) = (mkIdent (keyToText name),) <$> parseJSON ty
instance JSON.FromJSON Expression where
parseJSON v = bool v <|> integer v <|> concrete v <|> obj v
@ -192,7 +193,7 @@ instance JSON.FromJSON Expression where
TagRecord ->
do fields <- o .: "data"
flip (withObject "record data") fields $
\fs -> Record <$> traverse parseJSON fs
\fs -> (Record . toHashMapTextKM) <$> traverse parseJSON fs
TagSequence ->
do contents <- o .: "data"
flip (withArray "sequence") contents $
@ -234,7 +235,7 @@ instance JSON.ToJSON Expression where
]
toJSON (Record fields) =
object [ "expression" .= TagRecord
, "data" .= object [ fieldName .= toJSON val
, "data" .= object [ keyFromText fieldName .= toJSON val
| (fieldName, val) <- HM.toList fields
]
]

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

@ -13,7 +13,6 @@ import qualified Data.Aeson as JSON
import Data.Aeson ((.=), (.:), (.!=), (.:?))
import Data.Aeson.Types (Parser, typeMismatch)
import Data.Functor ((<&>))
import qualified Data.HashMap.Strict as HM
import qualified Data.Text as T
import qualified Cryptol.Parser.AST as C
@ -27,6 +26,7 @@ import Cryptol.Utils.PP (pp)
import Cryptol.Utils.RecordMap (canonicalFields)
import qualified Argo.Doc as Doc
import CryptolServer.AesonCompat
newtype JSONSchema = JSONSchema Schema
@ -219,7 +219,7 @@ instance JSON.ToJSON JSONType where
JSON.object
[ "type" .= T.pack "record"
, "fields" .=
JSON.object [ T.pack (show (pp f)) .= JSONType ns t'
JSON.object [ keyFromText (T.pack (show (pp f))) .= JSONType ns t'
| (f, t') <- canonicalFields fields
]
]
@ -231,17 +231,17 @@ instance JSON.FromJSON JSONPType where
where
getType :: JSON.Value -> Parser (C.Type C.PName)
getType (JSON.Object o) =
case HM.lookup "type" o of
case lookupKM "type" o of
Just t -> asType t o
Nothing ->
case HM.lookup "prop" o of
case lookupKM "prop" o of
Just p -> asProp p o
Nothing -> fail "Expected type or prop key"
getType other = typeMismatch "object" other
asType "record" = \o -> C.TRecord <$> ((o .: "fields") >>= getFields)
where
getFields obj = recordFromFields <$> traverse (\(k, v) -> (mkIdent k,) . (emptyRange,) <$> getType v) (HM.toList obj)
getFields obj = recordFromFields <$> traverse (\(k, v) -> (mkIdent (keyToText k),) . (emptyRange,) <$> getType v) (toListKM obj)
asType "variable" = \o -> C.TUser <$> (name <$> o .: "name") <*> (map unJSONPType <$> (o .:? "arguments" .!= []))
asType "number" = \o -> C.TNum <$> (o .: "value")
asType "inf" = const $ pure $ C.TUser (name "inf") []

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

@ -25,12 +25,12 @@ import Data.ByteString (ByteString)
import qualified Data.ByteString.Char8 as B8
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.HashMap.Strict as HashMap
import Cryptol.Parser
import qualified Cryptol.TypeCheck.Type as TC
import Argo
import CryptolServer.AesonCompat
import CryptolServer.Data.Type
cryptolError :: ModuleError -> [ModuleWarning] -> JSONRPCException
@ -167,7 +167,7 @@ unwantedDefaults defs =
makeJSONRPCException
20210 "Execution would have required these defaults"
(Just (JSON.object ["defaults" .=
[ jsonTypeAndString ty <> HashMap.fromList ["parameter" .= pretty param]
[ jsonTypeAndString ty <> fromListKM ["parameter" .= pretty param]
| (param, ty) <- defs ] ]))
evalInParamMod :: [CM.Name] -> JSONRPCException
@ -204,6 +204,6 @@ cryptolParseErr expr err =
-- human-readable string
jsonTypeAndString :: TC.Type -> JSON.Object
jsonTypeAndString ty =
HashMap.fromList
fromListKM
[ "type" .= JSONSchema (TC.Forall [] [] ty)
, "type string" .= pretty ty ]

33
cryptol-remote-api/src/CryptolServer/Interrupt.hs Normal file
View File

@ -0,0 +1,33 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.Interrupt
( interruptServer
, interruptServerDescr
) where
import qualified Argo
import qualified Argo.Doc as Doc
import qualified Data.Aeson as JSON
import CryptolServer
------------------------------------------------------------------------
-- Interrupt All Threads Command
data InterruptServerParams = InterruptServerParams
instance JSON.FromJSON InterruptServerParams where
parseJSON =
JSON.withObject "params for \"interrupt\"" $
\_ -> pure InterruptServerParams
instance Doc.DescribedMethod InterruptServerParams () where
parameterFieldDescription = []
interruptServerDescr :: Doc.Block
interruptServerDescr =
Doc.Paragraph [Doc.Text "Interrupt the server, terminating it's current task (if one exists)."]
interruptServer :: InterruptServerParams -> CryptolNotification ()
interruptServer _ = CryptolNotification . const $ Argo.interruptAllThreads

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

@ -25,7 +25,8 @@ loadFileDescr :: Doc.Block
loadFileDescr = Doc.Paragraph [Doc.Text "Load the specified module (by file path)."]
loadFile :: LoadFileParams -> CryptolCommand ()
loadFile (LoadFileParams fn) =
loadFile (LoadFileParams fn) = do
resetTCSolver
void $ liftModuleCmd (loadModuleByPath fn)
newtype LoadFileParams
@ -49,7 +50,8 @@ loadModuleDescr :: Doc.Block
loadModuleDescr = Doc.Paragraph [Doc.Text "Load the specified module (by name)."]
loadModule :: LoadModuleParams -> CryptolCommand ()
loadModule (LoadModuleParams mn) =
loadModule (LoadModuleParams mn) = do
resetTCSolver
void $ liftModuleCmd (loadModuleByName mn)
newtype JSONModuleName

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

@ -12,7 +12,6 @@ import qualified Argo.Doc as Doc
import Data.Aeson hiding (Options)
import Data.Aeson.Types (Parser, typeMismatch)
import Data.Coerce
import qualified Data.HashMap.Strict as HM
import qualified Data.Text as T
import Cryptol.Eval(EvalOpts(..))
@ -20,6 +19,8 @@ import Cryptol.REPL.Monad (parseFieldOrder, parsePPFloatFormat)
import Cryptol.Utils.Logger (quietLogger)
import Cryptol.Utils.PP (PPOpts(..), PPFloatFormat(..), PPFloatExp(..), FieldOrder(..), defaultPPOpts)
import CryptolServer.AesonCompat
data Options = Options { optCallStacks :: Bool, optEvalOpts :: EvalOpts }
newtype JSONEvalOpts = JSONEvalOpts { getEvalOpts :: EvalOpts }
@ -40,7 +41,7 @@ newtypeField :: forall wrapped bare proxy.
(Coercible wrapped bare, FromJSON wrapped) =>
proxy wrapped bare ->
Object -> T.Text -> bare -> Parser bare
newtypeField _proxy o field def = unwrap (o .:! field) .!= def where
newtypeField _proxy o field def = unwrap (o .:! keyFromText field) .!= def where
unwrap :: Parser (Maybe wrapped) -> Parser (Maybe bare)
unwrap = coerce
@ -85,7 +86,7 @@ instance FromJSON a => FromJSON (WithOptions a) where
\o ->
WithOptions <$>
o .:! "options" .!= defaultOpts <*>
parseJSON (Object (HM.delete "options" o))
parseJSON (Object (deleteKM "options" o))
defaultOpts :: Options
defaultOpts = Options False theEvalOpts

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

@ -118,10 +118,10 @@ offlineProveSat proverName cmd hConsing = do
Left msg -> do
raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg
Right smtlib -> pure $ OfflineSMTQuery $ T.pack smtlib
Right w4Cfg -> do
Right _w4Cfg -> do
smtlibRef <- liftIO $ newIORef ("" :: Text)
result <- liftModuleCmd $
W4.satProveOffline w4Cfg hConsing False cmd $ \f -> do
W4.satProveOffline hConsing False cmd $ \f -> do
withRWTempFile "smtOutput.tmp" $ \h -> do
f h
hSeek h AbsoluteSeek 0

7
cryptol-remote-api/test_docker.sh
View File

@ -1,5 +1,7 @@
#!/bin/bash
set -euo pipefail
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
PROTO=${1:-"http"}
@ -25,10 +27,13 @@ pushd $DIR/python
NUM_FAILS=0
echo "Setting up python environment for remote server clients..."
poetry update
poetry install
export CRYPTOL_SERVER_URL="$PROTO://localhost:8080/"
poetry run python -m unittest discover tests/cryptol
echo "Running cryptol-remote-api tests with remote server at $CRYPTOL_SERVER_URL..."
poetry run python -m unittest discover --verbose tests/cryptol
if [ $? -ne 0 ]; then
NUM_FAILS=$(($NUM_FAILS+1))
fi

11
cryptol.cabal
View File

@ -1,6 +1,6 @@
Cabal-version: 2.4
Name: cryptol
Version: 2.11.0.99
Version: 2.12.0.99
Synopsis: Cryptol: The Language of Cryptography
Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
License: BSD-3-Clause
@ -9,7 +9,7 @@ Author: Galois, Inc.
Maintainer: cryptol@galois.com
Homepage: http://www.cryptol.net/
Bug-reports: https://github.com/GaloisInc/cryptol/issues
Copyright: 2013-2020 Galois Inc.
Copyright: 2013-2021 Galois Inc.
Category: Language
Build-type: Simple
extra-source-files: bench/data/*.cry
@ -63,10 +63,10 @@ library
monad-control >= 1.0,
monadLib >= 3.7.2,
parameterized-utils >= 2.0.2,
pretty >= 1.1,
prettyprinter >= 1.7.0,
process >= 1.2,
sbv >= 8.10 && < 8.16,
simple-smt >= 0.7.1,
sbv >= 8.10 && < 8.17,
simple-smt >= 0.9.7,
stm >= 2.4,
strict,
text >= 1.1,
@ -232,6 +232,7 @@ executable cryptol
, directory
, filepath
, haskeline >= 0.7 && < 0.9
, exceptions
, monad-control
, text
, transformers

4
cryptol/REPL/Haskeline.hs
View File

@ -16,7 +16,7 @@ module REPL.Haskeline where
import Cryptol.REPL.Command
import Cryptol.REPL.Monad
import Cryptol.REPL.Trie
import Cryptol.Utils.PP
import Cryptol.Utils.PP hiding ((</>))
import Cryptol.Utils.Logger(stdoutLogger)
import Cryptol.Utils.Ident(modNameToText, interactiveName)
@ -99,7 +99,7 @@ getInputLines :: String -> InputT REPL NextLine
getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []
where
loop ls prompt =
do mb <- getInputLine prompt
do mb <- fmap (filter (/= '\r')) <$> getInputLine prompt
let newPropmpt = map (\_ -> ' ') prompt
case mb of
Nothing -> return NoMoreLines

2
deps/argo vendored

@ -1 +1 @@
Subproject commit 2481c42506c46be8b6562ab9dcef99fe85a54e5f
Subproject commit afee6bb49c7831a38316221e7b9721fbc65e88d7

0
docs/.nojekyll Normal file
View File

39
docs/CryptolPrims.md
View File

@ -25,13 +25,20 @@ Literals
number : {val, rep} Literal val rep => rep
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
// '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'
// '[x..y]' is syntactic sugar for 'fromTo`{first=x,last=y}'
fromTo : {first, last, a}
(fin last, last >= first,
Literal first a, Literal last a) =>
[1 + (last - first)]a
// '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'
// '[x .. < y]' is syntactic sugar for
// 'fromToLessThan`{first=x,bound=y}'
fromToLessThan : {first, bound, a}
(fin first, bound >= first, LiteralLessThan bound a) =>
[bound - first]a
// '[x,y..z]' is syntactic sugar for
// 'fromThenTo`{first=x,next=y,last=z}'
fromThenTo : {first, next, last, a, len}
( fin first, fin next, fin last
, Literal first a, Literal next a, Literal last a
@ -39,10 +46,30 @@ Literals
, lengthFromThenTo first next last == len) =>
[len]a
// '[a .. < b]` is syntactic sugar for 'fromToLessThan`{first=a,bound=b}'
fromToLessThan : {first, bound, a}
(fin first, bound >= first, LiteralLessThan bound a) =>
[bound - first]a
// '[x .. y by n]' is syntactic sugar for
// 'fromToBy`{first=x,last=y,stride=n}'.
primitive fromToBy : {first, last, stride, a}
(fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
[1 + (last - first)/stride]a
// '[x ..< y by n]' is syntactic sugar for
// 'fromToByLessThan`{first=x,bound=y,stride=n}'.
primitive fromToByLessThan : {first, bound, stride, a}
(fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
[(bound - first)/^stride]a
// '[x .. y down by n]' is syntactic sugar for
// 'fromToDownBy`{first=x,last=y,stride=n}'.
primitive fromToDownBy : {first, last, stride, a}
(fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
[1 + (first - last)/stride]a
// '[x ..> y down by n]' is syntactic sugar for
// 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.
primitive fromToDownByGreaterThan : {first, bound, stride, a}
(fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
[(first - bound)/^stride]a
Fractional Literals
-------------------

BIN
docs/CryptolPrims.pdf
View File

Binary file not shown.

BIN
docs/ProgrammingCryptol.pdf
View File

Binary file not shown.

257
docs/ProgrammingCryptol/appendices/Syntax.tex
View File

@ -2,7 +2,8 @@
% markdown in ../../Syntax.md. If you make changes, please make them
% there and then regenerate the .tex file using the Makefile.
\section{Layout}\label{layout}
\hypertarget{layout}{%
\section{Layout}\label{layout}}
Groups of declarations are organized based on indentation. Declarations
with the same indentation belong to the same group. Lines of text that
@ -32,7 +33,8 @@ containing \texttt{y} and \texttt{z}. This group ends just before
\texttt{g}, because \texttt{g} is indented less than \texttt{y} and
\texttt{z}.
\section{Comments}\label{comments}
\hypertarget{comments}{%
\section{Comments}\label{comments}}
Cryptol supports block comments, which start with \texttt{/*} and end
with \texttt{*/}, and line comments, which start with \texttt{//} and
@ -47,7 +49,8 @@ Examples:
/* This is a /* Nested */ block comment */
\end{verbatim}
\section{Identifiers}\label{identifiers}
\hypertarget{identifiers}{%
\section{Identifiers}\label{identifiers}}
Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (\texttt{\_}).
@ -64,8 +67,9 @@ name name1 name' longer_name
Name Name2 Name'' longerName
\end{verbatim}
\hypertarget{keywords-and-built-in-operators}{\section{Keywords and
Built-in Operators}\label{keywords-and-built-in-operators}}
\hypertarget{keywords-and-built-in-operators}{%
\section{Keywords and Built-in
Operators}\label{keywords-and-built-in-operators}}
The following identifiers have special meanings in Cryptol, and may not
be used for programmer defined names:
@ -73,8 +77,8 @@ be used for programmer defined names:
\begin{verbatim}
else include property let infixl parameter
extern module then import infixr constraint
if newtype type as infix
private pragma where hiding primitive
if newtype type as infix by
private pragma where hiding primitive down
\end{verbatim}
The following table contains Cryptol's operators and their associativity
@ -83,41 +87,40 @@ with lowest precedence operators first, and highest precedence last.
\begin{longtable}[]{@{}ll@{}}
\caption{Operator precedences.}\tabularnewline
\toprule
Operator & Associativity\tabularnewline
Operator & Associativity \\
\midrule
\endfirsthead
\toprule
Operator & Associativity\tabularnewline
Operator & Associativity \\
\midrule
\endhead
\texttt{==\textgreater{}} & right\tabularnewline
\texttt{\textbackslash{}/} & right\tabularnewline
\texttt{/\textbackslash{}} & right\tabularnewline
\texttt{==} \texttt{!=} \texttt{===} \texttt{!==} & not
associative\tabularnewline
\texttt{==\textgreater{}} & right \\
\texttt{\textbackslash{}/} & right \\
\texttt{/\textbackslash{}} & right \\
\texttt{==} \texttt{!=} \texttt{===} \texttt{!==} & not associative \\
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} \texttt{\textless{}\$}
\texttt{\textgreater{}\$} \texttt{\textless{}=\$}
\texttt{\textgreater{}=\$} & not associative\tabularnewline
\texttt{\textbar{}\textbar{}} & right\tabularnewline
\texttt{\^{}} & left\tabularnewline
\texttt{\&\&} & right\tabularnewline
\texttt{\#} & right\tabularnewline
\texttt{\textgreater{}=\$} & not associative \\
\texttt{\textbar{}\textbar{}} & right \\
\texttt{\^{}} & left \\
\texttt{\&\&} & right \\
\texttt{\#} & right \\
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\$} & left\tabularnewline
\texttt{+} \texttt{-} & left\tabularnewline
\texttt{*} \texttt{/} \texttt{\%} \texttt{/\$} \texttt{\%\$} &
left\tabularnewline
\texttt{\^{}\^{}} & right\tabularnewline
\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left\tabularnewline
(unary) \texttt{-} \texttt{\textasciitilde{}} & right\tabularnewline
\texttt{\textgreater{}\textgreater{}\$} & left \\
\texttt{+} \texttt{-} & left \\
\texttt{*} \texttt{/} \texttt{\%} \texttt{/\$} \texttt{\%\$} & left \\
\texttt{\^{}\^{}} & right \\
\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left \\
(unary) \texttt{-} \texttt{\textasciitilde{}} & right \\
\bottomrule
\end{longtable}
\hypertarget{built-in-type-level-operators}{%
\section{Built-in Type-level
Operators}\label{built-in-type-level-operators}
Operators}\label{built-in-type-level-operators}}
Cryptol includes a variety of operators that allow computations on the
numeric types used to specify the sizes of sequences.
@ -125,29 +128,30 @@ numeric types used to specify the sizes of sequences.
\begin{longtable}[]{@{}ll@{}}
\caption{Type-level operators}\tabularnewline
\toprule
Operator & Meaning\tabularnewline
Operator & Meaning \\
\midrule
\endfirsthead
\toprule
Operator & Meaning\tabularnewline
Operator & Meaning \\
\midrule
\endhead
\texttt{+} & Addition\tabularnewline
\texttt{-} & Subtraction\tabularnewline
\texttt{*} & Multiplication\tabularnewline
\texttt{/} & Division\tabularnewline
\texttt{/\^{}} & Ceiling division (\texttt{/} rounded up)\tabularnewline
\texttt{\%} & Modulus\tabularnewline
\texttt{\%\^{}} & Ceiling modulus (compute padding)\tabularnewline
\texttt{\^{}\^{}} & Exponentiation\tabularnewline
\texttt{lg2} & Ceiling logarithm (base 2)\tabularnewline
\texttt{width} & Bit width (equal to \texttt{lg2(n+1)})\tabularnewline
\texttt{max} & Maximum\tabularnewline
\texttt{min} & Minimum\tabularnewline
\texttt{+} & Addition \\
\texttt{-} & Subtraction \\
\texttt{*} & Multiplication \\
\texttt{/} & Division \\
\texttt{/\^{}} & Ceiling division (\texttt{/} rounded up) \\
\texttt{\%} & Modulus \\
\texttt{\%\^{}} & Ceiling modulus (compute padding) \\
\texttt{\^{}\^{}} & Exponentiation \\
\texttt{lg2} & Ceiling logarithm (base 2) \\
\texttt{width} & Bit width (equal to \texttt{lg2(n+1)}) \\
\texttt{max} & Maximum \\
\texttt{min} & Minimum \\
\bottomrule
\end{longtable}
\section{Numeric Literals}\label{numeric-literals}
\hypertarget{numeric-literals}{%
\section{Numeric Literals}\label{numeric-literals}}
Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
@ -226,7 +230,8 @@ some examples:
0x_FFFF_FFEA
\end{verbatim}
\section{Expressions}\label{expressions}
\hypertarget{expressions}{%
\section{Expressions}\label{expressions}}
This section provides an overview of the Cryptol's expression syntax.
@ -302,7 +307,8 @@ f \x -> x // call `f` with one argument `x -> x`
else z // call `+` with two arguments: `2` and `if ...`
\end{verbatim}
\section{Bits}\label{bits}
\hypertarget{bits}{%
\section{Bits}\label{bits}}
The type \texttt{Bit} has two inhabitants: \texttt{True} and
\texttt{False}. These values may be combined using various logical
@ -311,29 +317,30 @@ operators, or constructed as results of comparisons.
\begin{longtable}[]{@{}lll@{}}
\caption{Bit operations.}\tabularnewline
\toprule
Operator & Associativity & Description\tabularnewline
Operator & Associativity & Description \\
\midrule
\endfirsthead
\toprule
Operator & Associativity & Description\tabularnewline
Operator & Associativity & Description \\
\midrule
\endhead
\texttt{==\textgreater{}} & right & Short-cut implication\tabularnewline
\texttt{\textbackslash{}/} & right & Short-cut or\tabularnewline
\texttt{/\textbackslash{}} & right & Short-cut and\tabularnewline
\texttt{!=} \texttt{==} & none & Not equals, equals\tabularnewline
\texttt{==\textgreater{}} & right & Short-cut implication \\
\texttt{\textbackslash{}/} & right & Short-cut or \\
\texttt{/\textbackslash{}} & right & Short-cut and \\
\texttt{!=} \texttt{==} & none & Not equals, equals \\
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} \texttt{\textless{}\$}
\texttt{\textgreater{}\$} \texttt{\textless{}=\$}
\texttt{\textgreater{}=\$} & none & Comparisons\tabularnewline
\texttt{\textbar{}\textbar{}} & right & Logical or\tabularnewline
\texttt{\^{}} & left & Exclusive-or\tabularnewline
\texttt{\&\&} & right & Logical and\tabularnewline
\texttt{\textasciitilde{}} & right & Logical negation\tabularnewline
\texttt{\textgreater{}=\$} & none & Comparisons \\
\texttt{\textbar{}\textbar{}} & right & Logical or \\
\texttt{\^{}} & left & Exclusive-or \\
\texttt{\&\&} & right & Logical and \\
\texttt{\textasciitilde{}} & right & Logical negation \\
\bottomrule
\end{longtable}
\section{Multi-way Conditionals}\label{multi-way-conditionals}
\hypertarget{multi-way-conditionals}{%
\section{Multi-way Conditionals}\label{multi-way-conditionals}}
The \texttt{if\ ...\ then\ ...\ else} construct can be used with
multiple branches. For example:
@ -347,7 +354,8 @@ x = if y % 2 == 0 then 1
else 7
\end{verbatim}
\section{Tuples and Records}\label{tuples-and-records}
\hypertarget{tuples-and-records}{%
\section{Tuples and Records}\label{tuples-and-records}}
Tuples and records are used for packaging multiple values together.
Tuples are enclosed in parentheses, while records are enclosed in curly
@ -379,7 +387,8 @@ Ordering on tuples and records is defined lexicographically. Tuple
components are compared in the order they appear, whereas record fields
are compared in alphabetical order of field names.
\subsection{Accessing Fields}\label{accessing-fields}
\hypertarget{accessing-fields}{%
\subsection{Accessing Fields}\label{accessing-fields}}
The components of a record or a tuple may be accessed in two ways: via
pattern matching or by using explicit component selectors. Explicit
@ -441,7 +450,8 @@ only the first entry in the tuple.
This behavior is quite handy when examining complex data at the REPL.
\subsection{Updating Fields}\label{updating-fields}
\hypertarget{updating-fields}{%
\subsection{Updating Fields}\label{updating-fields}}
The components of a record or a tuple may be updated using the following
notation:
@ -464,7 +474,8 @@ n = { pt = r, size = 100 } // nested record
{ n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 }
\end{verbatim}
\section{Sequences}\label{sequences}
\hypertarget{sequences}{%
\section{Sequences}\label{sequences}}
A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length \texttt{n}, with elements of
@ -475,19 +486,25 @@ with elements of type \texttt{a} has type \texttt{{[}inf{]}\ a}, and
\texttt{{[}inf{]}} is an infinite stream of bits.
\begin{verbatim}
[e1,e2,e3] // A sequence with three elements
[e1,e2,e3] // A sequence with three elements
[t1 .. t3 ] // Sequence enumerations
[t1, t2 .. t3 ] // Step by t2 - t1
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[t1 .. t2] // Enumeration
[t1 .. <t2] // Enumeration (exclusive bound)
[t1 .. t2 by n] // Enumeration (stride)
[t1 .. <t2 by n] // Enumeration (stride, ex. bound)
[t1 .. t2 down by n] // Enumeration (downward stride)
[t1 .. >t2 down by n] // Enumeration (downward stride, ex. bound)
[t1, t2 .. t3] // Enumeration (step by t2 - t1)
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
[e1 ...] // Infinite sequence starting at e1
[e1, e2 ...] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
\end{verbatim}
Note: the bounds in finite sequences (those with \texttt{..}) are type
@ -497,28 +514,26 @@ expressions.
\begin{longtable}[]{@{}ll@{}}
\caption{Sequence operations.}\tabularnewline
\toprule
Operator & Description\tabularnewline
Operator & Description \\
\midrule
\endfirsthead
\toprule
Operator & Description\tabularnewline
Operator & Description \\
\midrule
\endhead
\texttt{\#} & Sequence concatenation\tabularnewline
\texttt{\#} & Sequence concatenation \\
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
Shift (right, left)\tabularnewline
Shift (right, left) \\
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}} & Rotate (right,
left)\tabularnewline
\texttt{\textless{}\textless{}\textless{}} & Rotate (right, left) \\
\texttt{\textgreater{}\textgreater{}\$} & Arithmetic right shift (on
bitvectors only)\tabularnewline
\texttt{@} \texttt{!} & Access elements (front, back)\tabularnewline
\texttt{@@} \texttt{!!} & Access sub-sequence (front,
back)\tabularnewline
bitvectors only) \\
\texttt{@} \texttt{!} & Access elements (front, back) \\
\texttt{@@} \texttt{!!} & Access sub-sequence (front, back) \\
\texttt{update} \texttt{updateEnd} & Update the value of a sequence at a
location (front, back)\tabularnewline
location (front, back) \\
\texttt{updates} \texttt{updatesEnd} & Update multiple values of a
sequence (front, back)\tabularnewline
sequence (front, back) \\
\bottomrule
\end{longtable}
@ -529,14 +544,16 @@ There are also lifted pointwise operations.
p1 # p2 // Split sequence pattern
\end{verbatim}
\section{Functions}\label{functions}
\hypertarget{functions}{%
\section{Functions}\label{functions}}
\begin{verbatim}
\p1 p2 -> e // Lambda expression
f p1 p2 = e // Function definition
\end{verbatim}
\section{Local Declarations}\label{local-declarations}
\hypertarget{local-declarations}{%
\section{Local Declarations}\label{local-declarations}}
\begin{verbatim}
e where ds
@ -546,7 +563,9 @@ Note that by default, any local declarations without type signatures are
monomorphized. If you need a local declaration to be polymorphic, use an
explicit type signature.
\section{Explicit Type Instantiation}\label{explicit-type-instantiation}
\hypertarget{explicit-type-instantiation}{%
\section{Explicit Type
Instantiation}\label{explicit-type-instantiation}}
If \texttt{f} is a polymorphic value with type:
@ -561,8 +580,9 @@ you can evaluate \texttt{f}, passing it a type parameter:
f `{ tyParam = 13 }
\end{verbatim}
\hypertarget{demoting-numeric-types-to-values}{%
\section{Demoting Numeric Types to
Values}\label{demoting-numeric-types-to-values}
Values}\label{demoting-numeric-types-to-values}}
The value corresponding to a numeric type may be accessed using the
following notation:
@ -571,15 +591,26 @@ following notation:
`t
\end{verbatim}
Here \texttt{t} should be a type expression with numeric kind. The
resulting expression is a finite word, which is sufficiently large to
accommodate the value of the type:
Here \texttt{t} should be a finite type expression with numeric kind.
The resulting expression will be of a numeric base type, which is
sufficiently large to accommodate the value of the type:
\begin{verbatim}
`t : {n} (fin n, n >= width t) => [n]
`t : {a} (Literal t a) => a
\end{verbatim}
\section{Explicit Type Annotations}\label{explicit-type-annotations}
This backtick notation is syntax sugar for an application of the
\texttt{number} primtive, so the above may be written as:
\begin{verbatim}
number`{t} : {a} (Literal t a) => a
\end{verbatim}
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually \texttt{Integer}.
\hypertarget{explicit-type-annotations}{%
\section{Explicit Type Annotations}\label{explicit-type-annotations}}
Explicit type annotations may be added on expressions, patterns, and in
argument definitions.
@ -592,15 +623,18 @@ p : t
f (x : t) = ...
\end{verbatim}
\section{Type Signatures}\label{type-signatures}
\hypertarget{type-signatures}{%
\section{Type Signatures}\label{type-signatures}}
\begin{verbatim}
f,g : {a,b} (fin a) => [a] b
\end{verbatim}
\section{Type Synonyms and Newtypes}\label{type-synonyms-and-newtypes}
\hypertarget{type-synonyms-and-newtypes}{%
\section{Type Synonyms and Newtypes}\label{type-synonyms-and-newtypes}}
\subsection{Type synonyms}\label{type-synonyms}
\hypertarget{type-synonyms}{%
\subsection{Type synonyms}\label{type-synonyms}}
\begin{verbatim}
type T a b = [a] b
@ -613,7 +647,8 @@ had instead written the body of the type synonym in line. Type synonyms
may mention other synonyms, but it is not allowed to create a recursive
collection of type synonyms.
\subsection{Newtypes}\label{newtypes}
\hypertarget{newtypes}{%
\subsection{Newtypes}\label{newtypes}}
\begin{verbatim}
newtype NewT a b = { seq : [a]b }
@ -647,7 +682,8 @@ of newtypes to extract the values in the body of the type.
6
\end{verbatim}
\section{Modules}\label{modules}
\hypertarget{modules}{%
\section{Modules}\label{modules}}
A \textbf{\emph{module}} is used to group some related definitions. Each
file may contain at most one module.
@ -661,7 +697,8 @@ f : [8]
f = 10
\end{verbatim}
\section{Hierarchical Module Names}\label{hierarchical-module-names}
\hypertarget{hierarchical-module-names}{%
\section{Hierarchical Module Names}\label{hierarchical-module-names}}
Module may have either simple or \textbf{\emph{hierarchical}} names.
Hierarchical names are constructed by gluing together ordinary
@ -680,7 +717,8 @@ when searching for module \texttt{Hash::SHA256}, Cryptol will look for a
file named \texttt{SHA256.cry} in a directory called \texttt{Hash},
contained in one of the directories specified by \texttt{CRYPTOLPATH}.
\section{Module Imports}\label{module-imports}
\hypertarget{module-imports}{%
\section{Module Imports}\label{module-imports}}
To use the definitions from one module in another module, we use
\texttt{import} declarations:
@ -701,7 +739,8 @@ import M // import all definitions from `M`
g = f // `f` was imported from `M`
\end{verbatim}
\section{Import Lists}\label{import-lists}
\hypertarget{import-lists}{%
\section{Import Lists}\label{import-lists}}
Sometimes, we may want to import only some of the definitions from a
module. To do so, we use an import declaration with an
@ -725,7 +764,8 @@ Using explicit import lists helps reduce name collisions. It also tends
to make code easier to understand, because it makes it easy to see the
source of definitions.
\section{Hiding Imports}\label{hiding-imports}
\hypertarget{hiding-imports}{%
\section{Hiding Imports}\label{hiding-imports}}
Sometimes a module may provide many definitions, and we want to use most
of them but with a few exceptions (e.g., because those would result to a
@ -748,7 +788,8 @@ import M hiding (h) // Import everything but `h`
x = f + g
\end{verbatim}
\section{Qualified Module Imports}\label{qualified-module-imports}
\hypertarget{qualified-module-imports}{%
\section{Qualified Module Imports}\label{qualified-module-imports}}
Another way to avoid name collisions is by using a
\textbf{\emph{qualified}} import.
@ -791,7 +832,8 @@ Such declarations will introduces all definitions from \texttt{A} and
\texttt{X} but to use them, you would have to qualify using the prefix
\texttt{B:::}.
\section{Private Blocks}\label{private-blocks}
\hypertarget{private-blocks}{%
\section{Private Blocks}\label{private-blocks}}
In some cases, definitions in a module might use helper functions that
are not intended to be used outside the module. It is good practice to
@ -832,7 +874,8 @@ private
helper2 = 3
\end{verbatim}
\section{Parameterized Modules}\label{parameterized-modules}
\hypertarget{parameterized-modules}{%
\section{Parameterized Modules}\label{parameterized-modules}}
\begin{verbatim}
module M where
@ -850,7 +893,9 @@ f : [n]
f = 1 + x
\end{verbatim}
\section{Named Module Instantiations}\label{named-module-instantiations}
\hypertarget{named-module-instantiations}{%
\section{Named Module
Instantiations}\label{named-module-instantiations}}
One way to use a parameterized module is through a named instantiation:
@ -887,8 +932,9 @@ Note that the only purpose of the body of \texttt{N} (the declarations
after the \texttt{where} keyword) is to define the parameters for
\texttt{M}.
\hypertarget{parameterized-instantiations}{%
\section{Parameterized
Instantiations}\label{parameterized-instantiations}
Instantiations}\label{parameterized-instantiations}}
It is possible for a module instantiation to be itself parameterized.
This could be useful if we need to define some of a module's parameters
@ -923,8 +969,9 @@ In this case \texttt{N} has a single parameter \texttt{x}. The result of
instantiating \texttt{N} would result in instantiating \texttt{M} using
the value of \texttt{x} and \texttt{12} for the value of \texttt{y}.
\hypertarget{importing-parameterized-modules}{%
\section{Importing Parameterized
Modules}\label{importing-parameterized-modules}
Modules}\label{importing-parameterized-modules}}
It is also possible to import a parameterized module without using a
module instantiation:

10
docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
View File

@ -97,7 +97,8 @@ Here is the response from Cryptol, in order:
\begin{small}
\begin{reploutVerb}
True
[error] at <interactive>:2:1--2:6 Value not in scope: false
[error] at <interactive>:2:1--2:6
Value not in scope: false
False
0x4
True
@ -790,7 +791,7 @@ Here are Cryptol's responses:
[]
invalid sequence index: 12
-- Backtrace --
(Cryptol::@) called at Cryptol:820:14--820:20
(Cryptol::@) called at Cryptol:875:14--875:20
(Cryptol::@@) called at <interactive>:9:1--9:28
[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
9
@ -1021,8 +1022,7 @@ the result:\indSignature
Cannot evaluate polymorphic value.
Type: {n, m, a} (n * m == 12, Literal 12 a, fin m) => [n][m]a
Cryptol> :t split [1..12]
split [1 .. 12] : {n, m, a} (n * m == 12, Literal 12 a, fin m) =>
[n][m]a
split [1 .. 12] : {n, m, a} (n * m == 12, Literal 12 a, fin m) => [n][m]a
\end{replPrompt}
%% cryptol 1 said: : {a b c} (fin c,c >= 4,a*b == 12) => [a][b][c]
@ -1795,7 +1795,7 @@ is subtly different from \texttt{[k, k+1...]}.
command to see the type Cryptol infers for this expression explicitly:
\begin{replPrompt}
Cryptol> :t [1:[_] .. 10]
[1 .. 10 : [_]] : {n} (n >= 4, n >= 1, fin n) => [10][n]
[1 .. 10 : [_]] : {n} (n >= 4, fin n) => [10][n]
\end{replPrompt}
Cryptol tells us that the sequence has precisely $10$ elements, and each
element is at least $4$ bits wide.

0
docs/RefMan/.gitignore vendored Normal file
View File

225
docs/RefMan/RefMan.rst
View File

@ -1,8 +1,3 @@
.. Cryptol Reference Manual documentation master file, created by
sphinx-quickstart on Thu Apr 29 15:31:18 2021.
You can adapt this file completely to your liking, but it should at least
contain the root `toctree` directive.
########################
Cryptol Reference Manual
########################
@ -22,7 +17,7 @@ Basic Syntax
Declarations
============
.. code-block:: cryptol
.. code-block:: cryptol
f x = x + y + z
@ -126,7 +121,8 @@ not be used for programmer defined names:
primitive
parameter
constraint
down
by
.. _Keywords:
.. code-block:: none
@ -134,8 +130,8 @@ not be used for programmer defined names:
else include property let infixl parameter
extern module then import infixr constraint
if newtype type as infix
private pragma where hiding primitive
if newtype type as infix down
private pragma where hiding primitive by
The following table contains Cryptol's operators and their
@ -246,7 +242,7 @@ type is inferred from context in which the literal is used. Examples:
0b1010 // : [4], 1 * number of digits
0o1234 // : [12], 3 * number of digits
0x1234 // : [16], 4 * number of digits
10 // : {a}. (Literal 10 a) => a
// a = Integer or [n] where n >= width 10
@ -356,7 +352,7 @@ in argument definitions.
then y
else z : Bit // the type annotation is on `z`, not the whole `if`
[1..9 : [8]] // specify that elements in `[1..9]` have type `[8]`
f (x : [8]) = x + 1 // type annotation on patterns
.. todo::
@ -442,15 +438,23 @@ following notation:
`t
Here ``t`` should be a type expression with numeric kind. The resulting
expression is a finite word, which is sufficiently large to accommodate
the value of the type:
Here `t` should be a finite type expression with numeric kind. The resulting
expression will be of a numeric base type, which is sufficiently large
to accommodate the value of the type:
.. code-block:: cryptol
`t : {n} (fin n, n >= width t) => [n]
`t : {a} (Literal t a) => a
This backtick notation is syntax sugar for an application of the
`number` primtive, so the above may be written as:
.. code-block:: cryptol
number`{t} : {a} (Literal t a) => a
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually `Integer`.
@ -507,7 +511,7 @@ sign. Examples:
(1,2,3) // A tuple with 3 component
() // A tuple with no components
{ x = 1, y = 2 } // A record with two fields, `x` and `y`
{} // A record with no fields
@ -520,7 +524,7 @@ Examples:
(1,2) == (1,2) // True
(1,2) == (2,1) // False
{ x = 1, y = 2 } == { x = 1, y = 2 } // True
{ x = 1, y = 2 } == { y = 2, x = 1 } // True
@ -539,7 +543,7 @@ component selectors are written as follows:
(15, 20).0 == 15
(15, 20).1 == 20
{ x = 15, y = 20 }.x == 15
Explicit record selectors may be used only if the program contains
@ -549,12 +553,12 @@ record. For example:
.. code-block:: cryptol
type T = { sign : Bit, number : [15] }
// Valid definition:
// the type of the record is known.
isPositive : T -> Bit
isPositive x = x.sign
// Invalid definition:
// insufficient type information.
badDef x = x.f
@ -567,9 +571,9 @@ patterns use braces. Examples:
.. code-block:: cryptol
getFst (x,_) = x
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
f p = x + y where
(x, y) = p
@ -605,14 +609,14 @@ notation:
r = { x = 15, y = 20 } // a record
t = (True,True) // a tuple
n = { pt = r, size = 100 } // nested record
// Setting fields
{ r | x = 30 } == { x = 30, y = 20 }
{ t | 0 = False } == (False,True)
// Update relative to the old value
{ r | x -> x + 5 } == { x = 20, y = 20 }
// Update a nested field
{ n | pt.x = 10 } == { pt = { x = 10, y = 20 }, size = 100 }
{ n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 }
@ -630,20 +634,25 @@ an infinite stream of bits.
.. code-block:: cryptol
[e1,e2,e3] // A sequence with three elements
[t1 .. t3 ] // Sequence enumerations
[t1, t2 .. t3 ] // Step by t2 - t1
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
[e1,e2,e3] // A sequence with three elements
[t1 .. t2] // Enumeration
[t1 .. <t2] // Enumeration (exclusive bound)
[t1 .. t2 by n] // Enumeration (stride)
[t1 .. <t2 by n] // Enumeration (stride, ex. bound)
[t1 .. t2 down by n] // Enumeration (downward stride)
[t1 .. >t2 down by n] // Enumeration (downward stride, ex. bound)
[t1, t2 .. t3] // Enumeration (step by t2 - t1)
[e1 ...] // Infinite sequence starting at e1
[e1, e2 ...] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
Note: the bounds in finite sequences (those with `..`) are type
expressions, while the bounds in infinite sequences are value
@ -658,7 +667,7 @@ expressions.
+------------------------------+---------------------------------------------+
| ``>>`` ``<<`` | Shift (right, left) |
+------------------------------+---------------------------------------------+
| ``>>>` ``<<<`` | Rotate (right, left) |
| ``>>>`` ``<<<`` | Rotate (right, left) |
+------------------------------+---------------------------------------------+
| ``>>$`` | Arithmetic right shift (on bitvectors only) |
+------------------------------+---------------------------------------------+
@ -692,6 +701,119 @@ Functions
f p1 p2 = e // Function definition
********************************************************************************
Overloaded Operations
********************************************************************************
Equality
========
.. code-block:: cryptol
Eq
(==) : {a} (Eq a) => a -> a -> Bit
(!=) : {a} (Eq a) => a -> a -> Bit
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
Comparisons
===========
.. code-block:: cryptol
Cmp
(<) : {a} (Cmp a) => a -> a -> Bit
(>) : {a} (Cmp a) => a -> a -> Bit
(<=) : {a} (Cmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
min : {a} (Cmp a) => a -> a -> a
max : {a} (Cmp a) => a -> a -> a
abs : {a} (Cmp a, Ring a) => a -> a
Signed Comparisons
==================
.. code-block:: cryptol
SignedCmp
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
Zero
====
.. code-block:: cryptol
Zero
zero : {a} (Zero a) => a
Logical Operations
==================
.. code-block:: cryptol
Logic
(&&) : {a} (Logic a) => a -> a -> a
(||) : {a} (Logic a) => a -> a -> a
(^) : {a} (Logic a) => a -> a -> a
complement : {a} (Logic a) => a -> a
Basic Arithmetic
================
.. code-block:: cryptol
Ring
fromInteger : {a} (Ring a) => Integer -> a
(+) : {a} (Ring a) => a -> a -> a
(-) : {a} (Ring a) => a -> a -> a
(*) : {a} (Ring a) => a -> a -> a
negate : {a} (Ring a) => a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
Integral Operations
===================
.. code-block:: cryptol
Integral
(/) : {a} (Integral a) => a -> a -> a
(%) : {a} (Integral a) => a -> a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
toInteger : {a} (Integral a) => a -> Integer
infFrom : {a} (Integral a) => a -> [inf]a
infFromThen : {a} (Integral a) => a -> a -> [inf]a
Division
========
.. code-block:: cryptol
Field
recip : {a} (Field a) => a -> a
(/.) : {a} (Field a) => a -> a -> a
Rounding
========
.. code-block:: cryptol
Round
ceiling : {a} (Round a) => a -> Integer
floor : {a} (Round a) => a -> Integer
trunc : {a} (Round a) => a -> Integer
roundAway : {a} (Round a) => a -> Integer
roundToEven : {a} (Round a) => a -> Integer
********************************************************************************
Type Declarations
********************************************************************************
@ -774,7 +896,7 @@ identifiers using the symbol ``::``.
.. code-block:: cryptol
module Hash::SHA256 where
sha256 = ...
The structure in the name may be used to group together related
@ -853,7 +975,7 @@ to use a *hiding* import:
:caption: module M
module M where
f = 0x02
g = 0x03
h = 0x04
@ -863,9 +985,9 @@ to use a *hiding* import:
:caption: module N
module N where
import M hiding (h) // Import everything but `h`
x = f + g
@ -880,7 +1002,7 @@ Another way to avoid name collisions is by using a
:caption: module M
module M where
f : [8]
f = 2
@ -889,9 +1011,9 @@ Another way to avoid name collisions is by using a
:caption: module N
module N where
import M as P
g = P::f
// `f` was imported from `M`
// but when used it needs to be prefixed by the qualifier `P`
@ -1097,20 +1219,20 @@ a module instantiation:
.. code-block:: cryptol
module M where
parameter
x : [8]
y : [8]
f : [8]
f = x + y
.. code-block:: cryptol
module N where
import `M
g = f { x = 2, y = 3 }
A *backtick* at the start of the name of an imported module indicates
@ -1121,3 +1243,6 @@ the parameters of a module. All value parameters are grouped in a record.
This is why in the example ``f`` is applied to a record of values,
even though its definition in ``M`` does not look like a function.

BIN
docs/RefMan/_build/doctrees/RefMan.doctree Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/environment.pickle Normal file
View File

Binary file not shown.

4
docs/RefMan/_build/html/.buildinfo Normal file
View File

@ -0,0 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: 3f9a4daf23c759ed9c684b18b96cc6ff
tags: 645f666f9bcd5a90fca523b33c5a78b7

0
docs/RefMan/_build/html/.nojekyll Normal file
View File

1411
docs/RefMan/_build/html/RefMan.html Normal file
View File

File diff suppressed because it is too large Load Diff

1248
docs/RefMan/_build/html/_sources/RefMan.rst.txt Normal file
View File

File diff suppressed because it is too large Load Diff

676
docs/RefMan/_build/html/_static/basic.css Normal file
View File

@ -0,0 +1,676 @@
/*
* basic.css
* ~~~~~~~~~
*
* Sphinx stylesheet -- basic theme.
*
* :copyright: Copyright 2007-2019 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
/* -- main layout ----------------------------------------------------------- */
div.clearer {
clear: both;
}
/* -- relbar ---------------------------------------------------------------- */
div.related {
width: 100%;
font-size: 90%;
}
div.related h3 {
display: none;
}
div.related ul {
margin: 0;
padding: 0 0 0 10px;
list-style: none;
}
div.related li {
display: inline;
}
div.related li.right {
float: right;
margin-right: 5px;
}
/* -- sidebar --------------------------------------------------------------- */
div.sphinxsidebarwrapper {
padding: 10px 5px 0 10px;
}
div.sphinxsidebar {
float: left;
width: 230px;
margin-left: -100%;
font-size: 90%;
word-wrap: break-word;
overflow-wrap : break-word;
}
div.sphinxsidebar ul {
list-style: none;
}
div.sphinxsidebar ul ul,
div.sphinxsidebar ul.want-points {
margin-left: 20px;
list-style: square;
}
div.sphinxsidebar ul ul {
margin-top: 0;
margin-bottom: 0;
}
div.sphinxsidebar form {
margin-top: 10px;
}
div.sphinxsidebar input {
border: 1px solid #98dbcc;
font-family: sans-serif;
font-size: 1em;
}
div.sphinxsidebar #searchbox form.search {
overflow: hidden;
}
div.sphinxsidebar #searchbox input[type="text"] {
float: left;
width: 80%;
padding: 0.25em;
box-sizing: border-box;
}
div.sphinxsidebar #searchbox input[type="submit"] {
float: left;
width: 20%;
border-left: none;
padding: 0.25em;
box-sizing: border-box;
}
img {
border: 0;
max-width: 100%;
}
/* -- search page ----------------------------------------------------------- */
ul.search {
margin: 10px 0 0 20px;
padding: 0;
}
ul.search li {
padding: 5px 0 5px 20px;
background-image: url(file.png);
background-repeat: no-repeat;
background-position: 0 7px;
}
ul.search li a {
font-weight: bold;
}
ul.search li div.context {
color: #888;
margin: 2px 0 0 30px;
text-align: left;
}
ul.keywordmatches li.goodmatch a {
font-weight: bold;
}
/* -- index page ------------------------------------------------------------ */
table.contentstable {
width: 90%;
margin-left: auto;
margin-right: auto;
}
table.contentstable p.biglink {
line-height: 150%;
}
a.biglink {
font-size: 1.3em;
}
span.linkdescr {
font-style: italic;
padding-top: 5px;
font-size: 90%;
}
/* -- general index --------------------------------------------------------- */
table.indextable {
width: 100%;
}
table.indextable td {
text-align: left;
vertical-align: top;
}
table.indextable ul {
margin-top: 0;
margin-bottom: 0;
list-style-type: none;
}
table.indextable > tbody > tr > td > ul {
padding-left: 0em;
}
table.indextable tr.pcap {
height: 10px;
}
table.indextable tr.cap {
margin-top: 10px;
background-color: #f2f2f2;
}
img.toggler {
margin-right: 3px;
margin-top: 3px;
cursor: pointer;
}
div.modindex-jumpbox {
border-top: 1px solid #ddd;
border-bottom: 1px solid #ddd;
margin: 1em 0 1em 0;
padding: 0.4em;
}
div.genindex-jumpbox {
border-top: 1px solid #ddd;
border-bottom: 1px solid #ddd;
margin: 1em 0 1em 0;
padding: 0.4em;
}
/* -- domain module index --------------------------------------------------- */
table.modindextable td {
padding: 2px;
border-collapse: collapse;
}
/* -- general body styles --------------------------------------------------- */
div.body {
min-width: 450px;
max-width: 800px;
}
div.body p, div.body dd, div.body li, div.body blockquote {
-moz-hyphens: auto;
-ms-hyphens: auto;
-webkit-hyphens: auto;
hyphens: auto;
}
a.headerlink {
visibility: hidden;
}
h1:hover > a.headerlink,
h2:hover > a.headerlink,
h3:hover > a.headerlink,
h4:hover > a.headerlink,
h5:hover > a.headerlink,
h6:hover > a.headerlink,
dt:hover > a.headerlink,
caption:hover > a.headerlink,
p.caption:hover > a.headerlink,
div.code-block-caption:hover > a.headerlink {
visibility: visible;
}
div.body p.caption {
text-align: inherit;
}
div.body td {
text-align: left;
}
.first {
margin-top: 0 !important;
}
p.rubric {
margin-top: 30px;
font-weight: bold;
}
img.align-left, .figure.align-left, object.align-left {
clear: left;
float: left;
margin-right: 1em;
}
img.align-right, .figure.align-right, object.align-right {
clear: right;
float: right;
margin-left: 1em;
}
img.align-center, .figure.align-center, object.align-center {
display: block;
margin-left: auto;
margin-right: auto;
}
.align-left {
text-align: left;
}
.align-center {
text-align: center;
}
.align-right {
text-align: right;
}
/* -- sidebars -------------------------------------------------------------- */
div.sidebar {
margin: 0 0 0.5em 1em;
border: 1px solid #ddb;
padding: 7px 7px 0 7px;
background-color: #ffe;
width: 40%;
float: right;
}
p.sidebar-title {
font-weight: bold;
}
/* -- topics ---------------------------------------------------------------- */
div.topic {
border: 1px solid #ccc;
padding: 7px 7px 0 7px;
margin: 10px 0 10px 0;
}
p.topic-title {
font-size: 1.1em;
font-weight: bold;
margin-top: 10px;
}
/* -- admonitions ----------------------------------------------------------- */
div.admonition {
margin-top: 10px;
margin-bottom: 10px;
padding: 7px;
}
div.admonition dt {
font-weight: bold;
}
div.admonition dl {
margin-bottom: 0;
}
p.admonition-title {
margin: 0px 10px 5px 0px;
font-weight: bold;
}
div.body p.centered {
text-align: center;
margin-top: 25px;
}
/* -- tables ---------------------------------------------------------------- */
table.docutils {
border: 0;
border-collapse: collapse;
}
table.align-center {
margin-left: auto;
margin-right: auto;
}
table caption span.caption-number {
font-style: italic;
}
table caption span.caption-text {
}
table.docutils td, table.docutils th {
padding: 1px 8px 1px 5px;
border-top: 0;
border-left: 0;
border-right: 0;
border-bottom: 1px solid #aaa;
}
table.footnote td, table.footnote th {
border: 0 !important;
}
th {
text-align: left;
padding-right: 5px;
}
table.citation {
border-left: solid 1px gray;
margin-left: 1px;
}
table.citation td {
border-bottom: none;
}
/* -- figures --------------------------------------------------------------- */
div.figure {
margin: 0.5em;
padding: 0.5em;
}
div.figure p.caption {
padding: 0.3em;
}
div.figure p.caption span.caption-number {
font-style: italic;
}
div.figure p.caption span.caption-text {
}
/* -- field list styles ----------------------------------------------------- */
table.field-list td, table.field-list th {
border: 0 !important;
}
.field-list ul {
margin: 0;
padding-left: 1em;
}
.field-list p {
margin: 0;
}
.field-name {
-moz-hyphens: manual;
-ms-hyphens: manual;
-webkit-hyphens: manual;
hyphens: manual;
}
/* -- hlist styles ---------------------------------------------------------- */
table.hlist td {
vertical-align: top;
}
/* -- other body styles ----------------------------------------------------- */
ol.arabic {
list-style: decimal;
}
ol.loweralpha {
list-style: lower-alpha;
}
ol.upperalpha {
list-style: upper-alpha;
}
ol.lowerroman {
list-style: lower-roman;
}
ol.upperroman {
list-style: upper-roman;
}
dl {
margin-bottom: 15px;
}
dd p {
margin-top: 0px;
}
dd ul, dd table {
margin-bottom: 10px;
}
dd {
margin-top: 3px;
margin-bottom: 10px;
margin-left: 30px;
}
dt:target, span.highlighted {
background-color: #fbe54e;
}
rect.highlighted {
fill: #fbe54e;
}
dl.glossary dt {
font-weight: bold;
font-size: 1.1em;
}
.optional {
font-size: 1.3em;
}
.sig-paren {
font-size: larger;
}
.versionmodified {
font-style: italic;
}
.system-message {
background-color: #fda;
padding: 5px;
border: 3px solid red;
}
.footnote:target {
background-color: #ffa;
}
.line-block {
display: block;
margin-top: 1em;
margin-bottom: 1em;
}
.line-block .line-block {
margin-top: 0;
margin-bottom: 0;
margin-left: 1.5em;
}
.guilabel, .menuselection {
font-family: sans-serif;
}
.accelerator {
text-decoration: underline;
}
.classifier {
font-style: oblique;
}
abbr, acronym {
border-bottom: dotted 1px;
cursor: help;
}
/* -- code displays --------------------------------------------------------- */
pre {
overflow: auto;
overflow-y: hidden; /* fixes display issues on Chrome browsers */
}
span.pre {
-moz-hyphens: none;
-ms-hyphens: none;
-webkit-hyphens: none;
hyphens: none;
}
td.linenos pre {
padding: 5px 0px;
border: 0;
background-color: transparent;
color: #aaa;
}
table.highlighttable {
margin-left: 0.5em;
}
table.highlighttable td {
padding: 0 0.5em 0 0.5em;
}
div.code-block-caption {
padding: 2px 5px;
font-size: small;
}
div.code-block-caption code {
background-color: transparent;
}
div.code-block-caption + div > div.highlight > pre {
margin-top: 0;
}
div.code-block-caption span.caption-number {
padding: 0.1em 0.3em;
font-style: italic;
}
div.code-block-caption span.caption-text {
}
div.literal-block-wrapper {
padding: 1em 1em 0;
}
div.literal-block-wrapper div.highlight {
margin: 0;
}
code.descname {
background-color: transparent;
font-weight: bold;
font-size: 1.2em;
}
code.descclassname {
background-color: transparent;
}
code.xref, a code {
background-color: transparent;
font-weight: bold;
}
h1 code, h2 code, h3 code, h4 code, h5 code, h6 code {
background-color: transparent;
}
.viewcode-link {
float: right;
}
.viewcode-back {
float: right;
font-family: sans-serif;
}
div.viewcode-block:target {
margin: -1px -10px;
padding: 0 10px;
}
/* -- math display ---------------------------------------------------------- */
img.math {
vertical-align: middle;
}
div.body div.math p {
text-align: center;
}
span.eqno {
float: right;
}
span.eqno a.headerlink {
position: relative;
left: 0px;
z-index: 1;
}
div.math:hover a.headerlink {
visibility: visible;
}
/* -- printout stylesheet --------------------------------------------------- */
@media print {
div.document,
div.documentwrapper,
div.bodywrapper {
margin: 0 !important;
width: 100%;
}
div.sphinxsidebar,
div.related,
div.footer,
#top-link {
display: none;
}
}

261
docs/RefMan/_build/html/_static/classic.css Normal file
View File

@ -0,0 +1,261 @@
/*
* classic.css_t
* ~~~~~~~~~~~~~
*
* Sphinx stylesheet -- classic theme.
*
* :copyright: Copyright 2007-2019 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
@import url("basic.css");
/* -- page layout ----------------------------------------------------------- */
body {
font-family: sans-serif;
font-size: 100%;
background-color: #11303d;
color: #000;
margin: 0;
padding: 0;
}
div.document {
background-color: #1c4e63;
}
div.documentwrapper {
float: left;
width: 100%;
}
div.bodywrapper {
margin: 0 0 0 230px;
}
div.body {
background-color: #ffffff;
color: #000000;
padding: 0 20px 30px 20px;
}
div.footer {
color: #ffffff;
width: 100%;
padding: 9px 0 9px 0;
text-align: center;
font-size: 75%;
}
div.footer a {
color: #ffffff;
text-decoration: underline;
}
div.related {
background-color: #133f52;
line-height: 30px;
color: #ffffff;
}
div.related a {
color: #ffffff;
}
div.sphinxsidebar {
}
div.sphinxsidebar h3 {
font-family: 'Trebuchet MS', sans-serif;
color: #ffffff;
font-size: 1.4em;
font-weight: normal;
margin: 0;
padding: 0;
}
div.sphinxsidebar h3 a {
color: #ffffff;
}
div.sphinxsidebar h4 {
font-family: 'Trebuchet MS', sans-serif;
color: #ffffff;
font-size: 1.3em;
font-weight: normal;
margin: 5px 0 0 0;
padding: 0;
}
div.sphinxsidebar p {
color: #ffffff;
}
div.sphinxsidebar p.topless {
margin: 5px 10px 10px 10px;
}
div.sphinxsidebar ul {
margin: 10px;
padding: 0;
color: #ffffff;
}
div.sphinxsidebar a {
color: #98dbcc;
}
div.sphinxsidebar input {
border: 1px solid #98dbcc;
font-family: sans-serif;
font-size: 1em;
}
/* -- hyperlink styles ------------------------------------------------------ */
a {
color: #355f7c;
text-decoration: none;
}
a:visited {
color: #355f7c;
text-decoration: none;
}
a:hover {
text-decoration: underline;
}
/* -- body styles ----------------------------------------------------------- */
div.body h1,
div.body h2,
div.body h3,
div.body h4,
div.body h5,
div.body h6 {
font-family: 'Trebuchet MS', sans-serif;
background-color: #f2f2f2;
font-weight: normal;
color: #20435c;
border-bottom: 1px solid #ccc;
margin: 20px -20px 10px -20px;
padding: 3px 0 3px 10px;
}
div.body h1 { margin-top: 0; font-size: 200%; }
div.body h2 { font-size: 160%; }
div.body h3 { font-size: 140%; }
div.body h4 { font-size: 120%; }
div.body h5 { font-size: 110%; }
div.body h6 { font-size: 100%; }
a.headerlink {
color: #c60f0f;
font-size: 0.8em;
padding: 0 4px 0 4px;
text-decoration: none;
}
a.headerlink:hover {
background-color: #c60f0f;
color: white;
}
div.body p, div.body dd, div.body li, div.body blockquote {
text-align: justify;
line-height: 130%;
}
div.admonition p.admonition-title + p {
display: inline;
}
div.admonition p {
margin-bottom: 5px;
}
div.admonition pre {
margin-bottom: 5px;
}
div.admonition ul, div.admonition ol {
margin-bottom: 5px;
}
div.note {
background-color: #eee;
border: 1px solid #ccc;
}
div.seealso {
background-color: #ffc;
border: 1px solid #ff6;
}
div.topic {
background-color: #eee;
}
div.warning {
background-color: #ffe4e4;
border: 1px solid #f66;
}
p.admonition-title {
display: inline;
}
p.admonition-title:after {
content: ":";
}
pre {
padding: 5px;
background-color: #eeffcc;
color: #333333;
line-height: 120%;
border: 1px solid #ac9;
border-left: none;
border-right: none;
}
code {
background-color: #ecf0f3;
padding: 0 1px 0 1px;
font-size: 0.95em;
}
th {
background-color: #ede;
}
.warning code {
background: #efc2c2;
}
.note code {
background: #d6d6d6;
}
.viewcode-back {
font-family: sans-serif;
}
div.viewcode-block:target {
background-color: #f4debf;
border-top: 1px solid #ac9;
border-bottom: 1px solid #ac9;
}
div.code-block-caption {
color: #efefef;
background-color: #1c4e63;
}

1
docs/RefMan/_build/html/_static/css/badge_only.css Normal file
View File

@ -0,0 +1 @@
.fa:before{-webkit-font-smoothing:antialiased}.clearfix{*zoom:1}.clearfix:after,.clearfix:before{display:table;content:""}.clearfix:after{clear:both}@font-face{font-family:FontAwesome;font-style:normal;font-weight:400;src:url(fonts/fontawesome-webfont.eot?674f50d287a8c48dc19ba404d20fe713?#iefix) format("embedded-opentype"),url(fonts/fontawesome-webfont.woff2?af7ae505a9eed503f8b8e6982036873e) format("woff2"),url(fonts/fontawesome-webfont.woff?fee66e712a8a08eef5805a46892932ad) format("woff"),url(fonts/fontawesome-webfont.ttf?b06871f281fee6b241d60582ae9369b9) format("truetype"),url(fonts/fontawesome-webfont.svg?912ec66d7572ff821749319396470bde#FontAwesome) format("svg")}.fa:before{font-family:FontAwesome;font-style:normal;font-weight:400;line-height:1}.fa:before,a .fa{text-decoration:inherit}.fa:before,a .fa,li .fa{display:inline-block}li .fa-large:before{width:1.875em}ul.fas{list-style-type:none;margin-left:2em;text-indent:-.8em}ul.fas li .fa{width:.8em}ul.fas li .fa-large:before{vertical-align:baseline}.fa-book:before,.icon-book:before{content:"\f02d"}.fa-caret-down:before,.icon-caret-down:before{content:"\f0d7"}.fa-caret-up:before,.icon-caret-up:before{content:"\f0d8"}.fa-caret-left:before,.icon-caret-left:before{content:"\f0d9"}.fa-caret-right:before,.icon-caret-right:before{content:"\f0da"}.rst-versions{position:fixed;bottom:0;left:0;width:300px;color:#fcfcfc;background:#1f1d1d;font-family:Lato,proxima-nova,Helvetica Neue,Arial,sans-serif;z-index:400}.rst-versions a{color:#2980b9;text-decoration:none}.rst-versions .rst-badge-small{display:none}.rst-versions .rst-current-version{padding:12px;background-color:#272525;display:block;text-align:right;font-size:90%;cursor:pointer;color:#27ae60}.rst-versions .rst-current-version:after{clear:both;content:"";display:block}.rst-versions .rst-current-version .fa{color:#fcfcfc}.rst-versions .rst-current-version .fa-book,.rst-versions .rst-current-version .icon-book{float:left}.rst-versions .rst-current-version.rst-out-of-date{background-color:#e74c3c;color:#fff}.rst-versions .rst-current-version.rst-active-old-version{background-color:#f1c40f;color:#000}.rst-versions.shift-up{height:auto;max-height:100%;overflow-y:scroll}.rst-versions.shift-up .rst-other-versions{display:block}.rst-versions .rst-other-versions{font-size:90%;padding:12px;color:grey;display:none}.rst-versions .rst-other-versions hr{display:block;height:1px;border:0;margin:20px 0;padding:0;border-top:1px solid #413d3d}.rst-versions .rst-other-versions dd{display:inline-block;margin:0}.rst-versions .rst-other-versions dd a{display:inline-block;padding:6px;color:#fcfcfc}.rst-versions.rst-badge{width:auto;bottom:20px;right:20px;left:auto;border:none;max-width:300px;max-height:90%}.rst-versions.rst-badge .fa-book,.rst-versions.rst-badge .icon-book{float:none;line-height:30px}.rst-versions.rst-badge.shift-up .rst-current-version{text-align:right}.rst-versions.rst-badge.shift-up .rst-current-version .fa-book,.rst-versions.rst-badge.shift-up .rst-current-version .icon-book{float:left}.rst-versions.rst-badge>.rst-current-version{width:auto;height:30px;line-height:30px;padding:0 6px;display:block;text-align:center}@media screen and (max-width:768px){.rst-versions{width:85%;display:none}.rst-versions.shift{display:block}}

BIN
docs/RefMan/_build/html/_static/css/fonts/Roboto-Slab-Bold.woff Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/Roboto-Slab-Bold.woff2 Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/Roboto-Slab-Regular.woff Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/Roboto-Slab-Regular.woff2 Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/fontawesome-webfont.eot Normal file
View File

Binary file not shown.

2671
docs/RefMan/_build/html/_static/css/fonts/fontawesome-webfont.svg Normal file
View File

File diff suppressed because it is too large Load Diff
Side by Side

After

Width:  |  Height:  |  Size: 434 KiB

BIN
docs/RefMan/_build/html/_static/css/fonts/fontawesome-webfont.ttf Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/fontawesome-webfont.woff Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/fontawesome-webfont.woff2 Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-bold-italic.woff Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-bold-italic.woff2 Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-bold.woff Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-bold.woff2 Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-normal-italic.woff Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-normal-italic.woff2 Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-normal.woff Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/css/fonts/lato-normal.woff2 Normal file
View File

Binary file not shown.

4
docs/RefMan/_build/html/_static/css/theme.css Normal file
View File

File diff suppressed because one or more lines are too long

315
docs/RefMan/_build/html/_static/doctools.js Normal file
View File

@ -0,0 +1,315 @@
/*
* doctools.js
* ~~~~~~~~~~~
*
* Sphinx JavaScript utilities for all documentation.
*
* :copyright: Copyright 2007-2019 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
/**
* select a different prefix for underscore
*/
$u = _.noConflict();
/**
* make the code below compatible with browsers without
* an installed firebug like debugger
if (!window.console || !console.firebug) {
var names = ["log", "debug", "info", "warn", "error", "assert", "dir",
"dirxml", "group", "groupEnd", "time", "timeEnd", "count", "trace",
"profile", "profileEnd"];
window.console = {};
for (var i = 0; i < names.length; ++i)
window.console[names[i]] = function() {};
}
*/
/**
* small helper function to urldecode strings
*/
jQuery.urldecode = function(x) {
return decodeURIComponent(x).replace(/\+/g, ' ');
};
/**
* small helper function to urlencode strings
*/
jQuery.urlencode = encodeURIComponent;
/**
* This function returns the parsed url parameters of the
* current request. Multiple values per key are supported,
* it will always return arrays of strings for the value parts.
*/
jQuery.getQueryParameters = function(s) {
if (typeof s === 'undefined')
s = document.location.search;
var parts = s.substr(s.indexOf('?') + 1).split('&');
var result = {};
for (var i = 0; i < parts.length; i++) {
var tmp = parts[i].split('=', 2);
var key = jQuery.urldecode(tmp[0]);
var value = jQuery.urldecode(tmp[1]);
if (key in result)
result[key].push(value);
else
result[key] = [value];
}
return result;
};
/**
* highlight a given string on a jquery object by wrapping it in
* span elements with the given class name.
*/
jQuery.fn.highlightText = function(text, className) {
function highlight(node, addItems) {
if (node.nodeType === 3) {
var val = node.nodeValue;
var pos = val.toLowerCase().indexOf(text);
if (pos >= 0 &&
!jQuery(node.parentNode).hasClass(className) &&
!jQuery(node.parentNode).hasClass("nohighlight")) {
var span;
var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg");
if (isInSVG) {
span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
} else {
span = document.createElement("span");
span.className = className;
}
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
node.parentNode.insertBefore(span, node.parentNode.insertBefore(
document.createTextNode(val.substr(pos + text.length)),
node.nextSibling));
node.nodeValue = val.substr(0, pos);
if (isInSVG) {
var bbox = span.getBBox();
var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect");
rect.x.baseVal.value = bbox.x;
rect.y.baseVal.value = bbox.y;
rect.width.baseVal.value = bbox.width;
rect.height.baseVal.value = bbox.height;
rect.setAttribute('class', className);
var parentOfText = node.parentNode.parentNode;
addItems.push({
"parent": node.parentNode,
"target": rect});
}
}
}
else if (!jQuery(node).is("button, select, textarea")) {
jQuery.each(node.childNodes, function() {
highlight(this, addItems);
});
}
}
var addItems = [];
var result = this.each(function() {
highlight(this, addItems);
});
for (var i = 0; i < addItems.length; ++i) {
jQuery(addItems[i].parent).before(addItems[i].target);
}
return result;
};
/*
* backward compatibility for jQuery.browser
* This will be supported until firefox bug is fixed.
*/
if (!jQuery.browser) {
jQuery.uaMatch = function(ua) {
ua = ua.toLowerCase();
var match = /(chrome)[ \/]([\w.]+)/.exec(ua) ||
/(webkit)[ \/]([\w.]+)/.exec(ua) ||
/(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) ||
/(msie) ([\w.]+)/.exec(ua) ||
ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) ||
[];
return {
browser: match[ 1 ] || "",
version: match[ 2 ] || "0"
};
};
jQuery.browser = {};
jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true;
}
/**
* Small JavaScript module for the documentation.
*/
var Documentation = {
init : function() {
this.fixFirefoxAnchorBug();
this.highlightSearchWords();
this.initIndexTable();
if (DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) {
this.initOnKeyListeners();
}
},
/**
* i18n support
*/
TRANSLATIONS : {},
PLURAL_EXPR : function(n) { return n === 1 ? 0 : 1; },
LOCALE : 'unknown',
// gettext and ngettext don't access this so that the functions
// can safely bound to a different name (_ = Documentation.gettext)
gettext : function(string) {
var translated = Documentation.TRANSLATIONS[string];
if (typeof translated === 'undefined')
return string;
return (typeof translated === 'string') ? translated : translated[0];
},
ngettext : function(singular, plural, n) {
var translated = Documentation.TRANSLATIONS[singular];
if (typeof translated === 'undefined')
return (n == 1) ? singular : plural;
return translated[Documentation.PLURALEXPR(n)];
},
addTranslations : function(catalog) {
for (var key in catalog.messages)
this.TRANSLATIONS[key] = catalog.messages[key];
this.PLURAL_EXPR = new Function('n', 'return +(' + catalog.plural_expr + ')');
this.LOCALE = catalog.locale;
},
/**
* add context elements like header anchor links
*/
addContextElements : function() {
$('div[id] > :header:first').each(function() {
$('<a class="headerlink">\u00B6</a>').
attr('href', '#' + this.id).
attr('title', _('Permalink to this headline')).
appendTo(this);
});
$('dt[id]').each(function() {
$('<a class="headerlink">\u00B6</a>').
attr('href', '#' + this.id).
attr('title', _('Permalink to this definition')).
appendTo(this);
});
},
/**
* workaround a firefox stupidity
* see: https://bugzilla.mozilla.org/show_bug.cgi?id=645075
*/
fixFirefoxAnchorBug : function() {
if (document.location.hash && $.browser.mozilla)
window.setTimeout(function() {
document.location.href += '';
}, 10);
},
/**
* highlight the search words provided in the url in the text
*/
highlightSearchWords : function() {
var params = $.getQueryParameters();
var terms = (params.highlight) ? params.highlight[0].split(/\s+/) : [];
if (terms.length) {
var body = $('div.body');
if (!body.length) {
body = $('body');
}
window.setTimeout(function() {
$.each(terms, function() {
body.highlightText(this.toLowerCase(), 'highlighted');
});
}, 10);
$('<p class="highlight-link"><a href="javascript:Documentation.' +
'hideSearchWords()">' + _('Hide Search Matches') + '</a></p>')
.appendTo($('#searchbox'));
}
},
/**
* init the domain index toggle buttons
*/
initIndexTable : function() {
var togglers = $('img.toggler').click(function() {
var src = $(this).attr('src');
var idnum = $(this).attr('id').substr(7);
$('tr.cg-' + idnum).toggle();
if (src.substr(-9) === 'minus.png')
$(this).attr('src', src.substr(0, src.length-9) + 'plus.png');
else
$(this).attr('src', src.substr(0, src.length-8) + 'minus.png');
}).css('display', '');
if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) {
togglers.click();
}
},
/**
* helper function to hide the search marks again
*/
hideSearchWords : function() {
$('#searchbox .highlight-link').fadeOut(300);
$('span.highlighted').removeClass('highlighted');
},
/**
* make the url absolute
*/
makeURL : function(relativeURL) {
return DOCUMENTATION_OPTIONS.URL_ROOT + '/' + relativeURL;
},
/**
* get the current relative url
*/
getCurrentURL : function() {
var path = document.location.pathname;
var parts = path.split(/\//);
$.each(DOCUMENTATION_OPTIONS.URL_ROOT.split(/\//), function() {
if (this === '..')
parts.pop();
});
var url = parts.join('/');
return path.substring(url.lastIndexOf('/') + 1, path.length - 1);
},
initOnKeyListeners: function() {
$(document).keyup(function(event) {
var activeElementType = document.activeElement.tagName;
// don't navigate when in search box or textarea
if (activeElementType !== 'TEXTAREA' && activeElementType !== 'INPUT' && activeElementType !== 'SELECT') {
switch (event.keyCode) {
case 37: // left
var prevHref = $('link[rel="prev"]').prop('href');
if (prevHref) {
window.location.href = prevHref;
return false;
}
case 39: // right
var nextHref = $('link[rel="next"]').prop('href');
if (nextHref) {
window.location.href = nextHref;
return false;
}
}
}
});
}
};
// quick alias for translations
_ = Documentation.gettext;
$(document).ready(function() {
Documentation.init();
});

10
docs/RefMan/_build/html/_static/documentation_options.js Normal file
View File

@ -0,0 +1,10 @@
var DOCUMENTATION_OPTIONS = {
URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'),
VERSION: '2.11.0',
LANGUAGE: 'None',
COLLAPSE_INDEX: false,
FILE_SUFFIX: '.html',
HAS_SOURCE: true,
SOURCELINK_SUFFIX: '.txt',
NAVIGATION_WITH_KEYS: false,
};

BIN
docs/RefMan/_build/html/_static/file.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 286 B

BIN
docs/RefMan/_build/html/_static/fonts/Inconsolata-Bold.ttf Normal file
View File

Binary file not shown.

BIN
docs/RefMan/_build/html/_static/fonts/Inconsolata-Regular.ttf Normal file
View File

Binary file not shown.

Some files were not shown because too many files have changed in this diff Show More