Merge remote-tracking branch 'origin/master' into explicit-stride

.github/ci.sh

@@ -71,8 +71,9 @@ install_cvc4() {
   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/')"
-    curl -o cvc4$EXT -sSL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/$latest"
+    #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

.github/workflows/ci.yml

@@ -197,7 +197,7 @@ 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
@@ -208,10 +208,10 @@ jobs:
             target: ''
             os: macos-latest
             continue-on-error: false
-          - suite: rpc
-            target: ''
-            os: windows
-            continue-on-error: true  # TODO: get Python client to work on Windows
+          #- suite: rpc
+          #  target: ''
+          #  os: windows-latest
+          #  continue-on-error: true  # TODO: get Python client to work on Windows
     steps:
       - uses: actions/checkout@v2
         with:
@@ -349,7 +349,11 @@ jobs:
 
       - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
         name: Test cryptol-remote-api
-        run: ./cryptol-remote-api/test_docker.sh ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
+        run: ./cryptol-remote-api/test_docker.sh http ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
+
+      - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
+        name: Test cryptol-remote-api (TLS)
+        run: ./cryptol-remote-api/test_docker.sh https ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }}
 
       - if: matrix.image == 'ghcr.io/galoisinc/cryptol-remote-api'
         uses: docker/build-push-action@v2
@@ -391,13 +395,13 @@ jobs:
       - if: needs.config.outputs.event-schedule == 'true'
         name: ${{ matrix.image }}:nightly
         run: |
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:nightly
+          docker tag ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} ${{ matrix.image }}:nightly
           docker push ${{ matrix.image }}:nightly
 
       - if: needs.config.outputs.release == 'true'
         name: ${{ matrix.image }}:${{ needs.config.outputs.version }}
         run: |
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }}
+          docker tag ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} ${{ matrix.image }}:${{ needs.config.outputs.version }}
           docker push ${{ matrix.image }}:${{ needs.config.outputs.version }}
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest
+          docker tag ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} ${{ matrix.image }}:latest
           docker push ${{ matrix.image }}:latest

.gitpod.Dockerfile

@@ -0,0 +1,30 @@
+
+FROM gitpod/workspace-full
+
+# Install docker buildx plugin
+RUN mkdir -p ~/.docker/cli-plugins && \
+    wget \
+      https://github.com/docker/buildx/releases/download/v0.5.1/buildx-v0.5.1.linux-amd64 \
+      -O ~/.docker/cli-plugins/docker-buildx && \
+    chmod a+x ~/.docker/cli-plugins/docker-buildx
+
+USER root
+
+# Install Dropbear SSH server
+RUN apt-get update && DEBIAN_FRONTEND=noninteractive apt-get install -yq \
+        dropbear \
+    && apt-get clean && rm -rf /var/lib/apt/lists/* /tmp/*
+
+# Install Chisel
+RUN curl https://i.jpillora.com/chisel! | bash
+
+# Install GHC
+ARG GHCVER="8.10.3"
+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
+RUN ghcup install cabal --set
+ENV PATH=/root/.cabal/bin:$PATH
+RUN ghcup install ghc ${GHCVER} && \
+    ghcup set ghc ${GHCVER}

.gitpod.yml

@@ -0,0 +1,39 @@
+image:
+  file: .gitpod.Dockerfile
+vscode:
+  extensions:
+    - haskell.haskell
+    - justusadam.language-haskell
+tasks:
+  - name: TCP Tunnel
+    command: chisel server --socks5
+  - name: SSH Server
+    command: |
+      [ -f /workspace/dropbear.hostkey ] || dropbearkey -t rsa -f /workspace/dropbear.hostkey
+      dropbear -r /workspace/dropbear.hostkey -F -E -s -p 2222 -P ~/dropbear.pid
+  - command: |
+      cabal v2-update
+      test -e cabal.project.freeze && exit 0
+      FREEZE=cabal.GHC-$(ghc --numeric-version).config
+      test -e $FREEZE && ln -s $FREEZE cabal.project.freeze
+  - command: |
+      mkdir -p ~/.ssh
+      if test -z "$SSH_KEY"; then
+          echo "Warning: SSH_KEY not set, skipping SSH setup"
+      else
+          echo "$SSH_KEY" >> ~/.ssh/authorized_keys
+          echo "1. Install Chisel on your local machine, e.g. curl https://i.jpillora.com/chisel! | bash"
+          echo "   see https://github.com/jpillora/chisel"
+          echo ""
+          echo "2. Connect via SSH from your local machine:"
+          echo "   ssh -o ProxyCommand='chisel client $(gp url 8080) stdio:%h:%p' gitpod@localhost -p 2222"
+          echo ""
+      fi
+ports:
+  - port: 8080
+  - port: 2222
+    onOpen: ignore
+  - port: 2375
+    onOpen: ignore
+  - port: 43022
+    onOpen: ignore

Dockerfile

@@ -1,4 +1,4 @@
-FROM debian:buster AS solvers
+FROM debian:buster-20210511 AS solvers
 
 # Install needed packages for building
 RUN apt-get update \
@@ -32,7 +32,8 @@ RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux
 # 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="$(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.
@@ -73,7 +74,7 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
 USER root
 RUN chown -R root:root /cryptol/rootfs
 
-FROM debian:buster-slim
+FROM debian:buster-20210511-slim
 RUN apt-get update \
     && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 \
     && apt-get clean && rm -rf /var/lib/apt/lists/*

README.md

@@ -1,4 +1,6 @@
 [![Cryptol](https://github.com/GaloisInc/cryptol/workflows/Cryptol/badge.svg)](https://github.com/GaloisInc/cryptol/actions?query=workflow%3ACryptol)
+[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/GaloisInc/cryptol)
+
 
 # Cryptol, version 2
 

cryptol-remote-api/CHANGELOG.md

@@ -1,5 +1,11 @@
-# Revision history for cryptol-server
+# Revision history for `cryptol-remote-api` and `cryptol-eval-server`
 
-## 0.1.0.0 -- YYYY-mm-dd
+## 2.11.1 -- 2021-06-23
 
-* First version. Released on an unsuspecting world.
+* HTTPS/TLS support added. Enable by running server in `http` mode with `--tls`
+  flag or by setting an environment variable (command line `--help` contains details).
+
+
+## 2.11.0
+
+* First "released" version of `cryptol-remote-api`.

cryptol-remote-api/Dockerfile

@@ -1,6 +1,6 @@
 ARG GHCVER="8.10.3"
 ARG GHCVER_BOOTSTRAP="8.10.2"
-FROM debian:buster AS solvers
+FROM debian:buster-20210511 AS solvers
 
 # Install needed packages for building
 RUN apt-get update \
@@ -44,7 +44,7 @@ RUN latest="$(curl -sSL 'http://cvc4.cs.stanford.edu/downloads/builds/x86_64-lin
 # Set executable and run tests
 RUN chmod +x rootfs/usr/local/bin/*
 
-FROM debian:buster AS toolchain
+FROM debian:buster-20210511 AS toolchain
 ARG PORTABILITY=false
 RUN apt-get update && apt-get install -y libncurses-dev libz-dev \
     build-essential curl libffi-dev libffi6 libgmp-dev libgmp10 libncurses-dev libncurses5 libtinfo5 libnuma-dev \
@@ -81,7 +81,7 @@ RUN if ${PORTABILITY}; then \
 
 FROM toolchain AS build
 
-RUN useradd -m cryptol
+RUN useradd -u 1000 -m cryptol
 COPY --chown=cryptol:cryptol . /cryptol
 USER cryptol
 WORKDIR /cryptol
@@ -91,10 +91,11 @@ ENV LANG=C.UTF-8 \
     LC_ALL=C.UTF-8
 COPY cabal.GHC-${GHCVER}.config cabal.project.freeze
 
-RUN mkdir -p rootfs/usr/local/bin
+RUN if ${PORTABILITY}; then SERVERS_NOT_THREADED="true"; fi
 
 RUN cabal v2-update && \
-    cabal v2-build -j cryptol-remote-api:exe:cryptol-remote-api cryptol-remote-api:exe:cryptol-eval-server && \
+    cabal v2-build -j ${SERVERS_NOT_THREADED:+-fNotThreaded} cryptol-remote-api:exe:cryptol-remote-api cryptol-remote-api:exe:cryptol-eval-server && \
+    mkdir -p rootfs/usr/local/bin && \
     cp $(cabal v2-exec which cryptol-remote-api) rootfs/usr/local/bin && \
     cp $(cabal v2-exec which cryptol-eval-server) rootfs/usr/local/bin
 ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
@@ -103,9 +104,9 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
 USER root
 RUN chown -R root:root /cryptol/rootfs
 
-FROM debian:buster-slim
+FROM debian:buster-20210511-slim
 RUN apt-get update \
-    && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 libnuma-dev \
+    && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 libnuma-dev openssl \
     && apt-get clean && rm -rf /var/lib/apt/lists/*
 RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
 COPY --from=build /cryptol/rootfs /
@@ -115,5 +116,11 @@ ENV LANG=C.UTF-8 \
     LC_ALL=C.UTF-8
 ENTRYPOINT ["/usr/local/bin/cryptol-remote-api"]
 WORKDIR /home/cryptol
+# Create self-signed certificates for HTTPS testing purposes - N.B.,
+# clients must opt in to accepting these by passing `verify=False` to
+# the `cryptol.connect` method (otherwise a security error is raised).
+RUN openssl req -nodes -newkey rsa:2048 -keyout server.key -out server.csr \
+      -subj "/C=GB/ST=London/L=London/O=Acme Widgets/OU=IT Department/CN=localhost"
+RUN openssl x509 -req -days 365 -in server.csr -signkey server.key -out server.crt
 CMD ["http", "--host", "0.0.0.0", "--port", "8080", "/"]
 EXPOSE 8080

cryptol-remote-api/cryptol-remote-api.cabal

@@ -12,6 +12,11 @@ flag static
   default: False
   description: Create a statically-linked binary
 
+flag NotThreaded
+  default: false
+  manual: true
+  description: Omit the -threaded ghc flag
+
 common warnings
   ghc-options:
     -Wall
@@ -42,6 +47,7 @@ common deps
     bytestring           ^>= 0.10.8,
     containers           >=0.6.0.1 && <0.7,
     cryptol              >= 2.9.0,
+    directory,
     filepath             ^>= 1.4,
     lens                 >= 4.17 && < 4.20,
     mtl                  ^>= 2.2,
@@ -78,8 +84,10 @@ executable cryptol-remote-api
   import:              deps, warnings, errors
   main-is:             Main.hs
   hs-source-dirs:      cryptol-remote-api
-  ghc-options:
-    -threaded -rtsopts -with-rtsopts=-xb0x200000000
+  if flag(NotThreaded)
+    ghc-options: -rtsopts -with-rtsopts=-xb0x200000000
+  else
+    ghc-options: -threaded -rtsopts -with-rtsopts=-xb0x200000000
 
   build-depends:
     cryptol-remote-api,
@@ -92,8 +100,10 @@ executable cryptol-eval-server
   import:              deps, warnings, errors
   main-is:             Main.hs
   hs-source-dirs:      cryptol-eval-server
-  ghc-options:
-    -threaded -rtsopts
+  if flag(NotThreaded)
+    ghc-options: -rtsopts -with-rtsopts=-xb0x200000000
+  else
+    ghc-options: -threaded -rtsopts -with-rtsopts=-xb0x200000000
 
   build-depends:
     cryptol-remote-api,

cryptol-remote-api/docs/Cryptol.rst

@@ -13,39 +13,37 @@ The server supports three transport methods:
 
 
 ``stdio``
-  in which the server communicates over ``stdin`` and ``stdout``
+  in which the server communicates over ``stdin`` and ``stdout`` using `netstrings. <http://cr.yp.to/proto/netstrings.txt>`_
 
 
 
-Socket
-  in which the server communicates over ``stdin`` and ``stdout``
+``socket``
+  in which the server communicates over a socket using `netstrings. <http://cr.yp.to/proto/netstrings.txt>`_
 
 
 
-HTTP
-  in which the server communicates over HTTP
+``http``
+  in which the server communicates over a socket using HTTP.
 
 
-In both ``stdio`` and socket mode, messages are delimited using `netstrings. <http://cr.yp.to/proto/netstrings.txt>`_
-
 
 Application State
 ~~~~~~~~~~~~~~~~~
 
 According to the JSON-RPC specification, the ``params`` field in a message object must be an array or object. In this protocol, it is always an object. While each message may specify its own arguments, every message has a parameter field named ``state``.
 
-When the first message is sent from the client to the server, the ``state`` parameter should be initialized to the JSON null value ``null``. Replies from the server may contain a new state that should be used in subsequent requests, so that state changes executed by the request are visible. Prior versions of this protocol represented the initial state as the empty array ``[]``, but this is now deprecated and will be removed.
+When the first message is sent from the client to the server, the ``state`` parameter should be initialized to the JSON null value ``null``. Replies from the server may contain a new state that should be used in subsequent requests, so that state changes executed by the request are visible.
 
 In particular, per JSON-RPC, non-error replies are always a JSON object that contains a ``result`` field. The result field always contains an ``answer`` field and a ``state`` field, as well as ``stdout`` and ``stderr``.
 
 
 ``answer``
-  The value returned as a response to the request (the precise contents depend on which request was sent)
+  The value returned as a response to the request (the precise contents depend on which request was sent).
 
 
 
 ``state``
-  The state, to be sent in subsequent requests. If the server did not modify its state in response to the command, then this state may be the same as the one sent by the client.
+  The state, to be sent in subsequent requests. If the server did not modify its state in response to the command, then this state may be the same as the one sent by the client. When a new state is in a server response, the previous state may no longer be available for requests.
 
 
 
@@ -559,7 +557,7 @@ Parameter fields
 
 
 ``prover``
-  The SMT solver to use to check for satisfiability. I.e., one of the following: ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``, .
+  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``.
 
 
 
@@ -578,27 +576,37 @@ Parameter fields
 
 
 
+``hash consing``
+  Whether or not to use hash consing of terms (if available).``true`` to enable or ``false`` to disable.
+
+
+
 Return fields
 +++++++++++++
 
 
 ``result``
-  A string (one of ``unsatisfiable``, ``invalid``, or ``satisfied``) indicating the result of checking for validity, satisfiability, or safety.
+  Either a string indicating the result of checking for validity, satisfiability, or safety---i.e., one of ``unsatisfiable``, ``invalid``, or ``satisfied``---or the string literal ``offline`` indicating an offline solver option was selected and the contents of the SMT query will be returned instead of a SAT result.
 
 
 
 ``counterexample type``
-  Only used if the ``result`` is ``invalid``.This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``.
+  Only used if the ``result`` is ``invalid``. This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``.
 
 
 
 ``counterexample``
-  Only used if the ``result`` is ``invalid``.A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression.
+  Only used if the ``result`` is ``invalid``. A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression.
   
   
 
 ``models``
-  Only used if the ``result`` is ``satisfied``.A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression.
+  Only used if the ``result`` is ``satisfied``. A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression.
+  
+  
+
+``query``
+  Only used if the ``result`` is ``offline``. The raw textual contents of the requested SMT query which can inspected or manually given to an SMT solver.