Merge pull request #1550 from GaloisInc/rpc/quoted-cryptol

[RPC] Update with latest cryptol_client, fix types
GaloisInc · Jan 4, 2022 · f7a0de1 · f7a0de1
2 parents 1e4dd12 + a82497e
commit f7a0de1
Show file tree

Hide file tree

Showing 19 changed files with 249 additions and 195 deletions.
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock
diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml
@@ -14,8 +14,8 @@ include = [
 python = "^3.8"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-cryptol = "2.12.0" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
-argo-client = "~0.0.6"
+cryptol = "2.12.2" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
+argo-client = "0.0.10"
 
 [tool.poetry.dev-dependencies]
 mypy = "^0.812"

diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py
@@ -633,8 +633,7 @@ def prove(goal: cryptoltypes.CryptolJSON,
     argument.
     """
     conn = __get_designated_connection()
-    res = conn.prove(cryptoltypes.to_cryptol(goal),
-                     proof_script.to_json()).result()
+    res = conn.prove(goal, proof_script.to_json()).result()
     pr = ProofResult()
     if res['status'] == 'valid':
         pr.valid = True

diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py
@@ -177,7 +177,7 @@ def __init__(
             goal : cryptoltypes.CryptolJSON,
             script : ProofScript,
             timeout : Optional[float]) -> None:
-        params = {'goal': goal,
+        params = {'goal': cryptoltypes.to_cryptol(goal),
                   'script': script}
         super(Prove, self).__init__('SAW/prove', params, connection, timeout=timeout)
+5 −1		cryptol-remote-api/python/CHANGELOG.md
+224 −296		cryptol-remote-api/python/cryptol/cryptoltypes.py
+3 −15		cryptol-remote-api/python/cryptol/opaque.py
+1 −1		cryptol-remote-api/python/cryptol/single_connection.py
+2 −2		cryptol-remote-api/python/cryptol/synchronous.py
+1 −1		cryptol-remote-api/python/pyproject.toml
+3 −0		cryptol-remote-api/python/tests/cryptol/test-files/Types.cry
+2 −1		cryptol-remote-api/python/tests/cryptol/test_basics.py
+29 −1		cryptol-remote-api/python/tests/cryptol/test_types.py