Merge pull request #1200 from GaloisInc/wip/rpc/feat/newtype

initial newtype support for rpc server

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

@@ -63,6 +63,7 @@ library
     CryptolServer.Check
     CryptolServer.ClearState
     CryptolServer.Data.Expression
+    CryptolServer.Data.FreshName
     CryptolServer.Data.Type
     CryptolServer.EvalExpr
     CryptolServer.ExtendSearchPath

cryptol-remote-api/python/cryptol/commands.py

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

cryptol-remote-api/python/cryptol/cryptoltypes.py

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

cryptol-remote-api/python/cryptol/opaque.py

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

cryptol-remote-api/python/tests/cryptol/test-files/CplxQNewtype.cry

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

cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py

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

cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py

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