feature: use BV class as python value for Cryptol bit sequences (#116)

* feature: use BV class as python value for Cryptol bit sequences

* fix: correct subtraction bug and add test

* chore: fix typos, delete misc commented out code

* chore: use Sphinx-style docstrings

* test: add cryptol python unit tests to CI

* chore: rename module bv to bitvector

* chore: rename test for cryptol.bitvector

* feature: allow BV creation from size/value or a BitVector

* feature: add widen method to BV

* install python deps for CI

* chore: fix typo in widen docstrings

* feature: with_bits method for replacing segments of BVs

* chore: tweak all python tests to use cabal, fix mypy test failures

* feature: support BV keyword args for construction

* try tweaking the mypy version in requirements.txt...

.github/workflows/ci.yml

@@ -40,10 +40,16 @@ jobs:
       run: cabal update
       # Build macaw-base dependencies and crucible separately just so later
       # steps are less verbose and major dependency failures are separate.
+    - name: Install python dependencies
+      working-directory: ./python
+      run: |
+        if [ -f requirements.txt ]; then pip3 install -r requirements.txt; fi
     - name: Build
       run: |
         cabal build all
     - name: Cabal argo tests
       run: cabal test argo
     - name: Cabal file-echo-api tests
       run: cabal test file-echo-api
+    - name: Python unit tests
+      run: cabal test python

python/cryptol/__init__.py

@@ -13,7 +13,7 @@
 from argo.interaction import HasProtocolState
 from argo.connection import DynamicSocketProcess, ServerConnection, ServerProcess, StdIOProcess
 from . import cryptoltypes
-
+from cryptol.bitvector import BV
 
 
 __all__ = ['cryptoltypes']
@@ -42,6 +42,7 @@ def fail_with(x : Exception) -> NoReturn:
 
 
 def from_cryptol_arg(val : Any) -> Any:
+    """Return the canonical Python value for a Cryptol JSON value."""
     if isinstance(val, bool):
         return val
     elif isinstance(val, int):
@@ -58,13 +59,18 @@ def from_cryptol_arg(val : Any) -> Any:
             return [from_cryptol_arg(v) for v in val['data']]
         elif tag == 'bits':
             enc = val['encoding']
+            size = val['width']
             if enc == 'base64':
-                data = base64.b64decode(val['data'].encode('ascii'))
+                n = int.from_bytes(
+                        base64.b64decode(val['data'].encode('ascii')),
+                        byteorder='big')
             elif enc == 'hex':
-                data = bytes.fromhex(extend_hex(val['data']))
+                n = int.from_bytes(
+                    bytes.fromhex(extend_hex(val['data'])),
+                    byteorder='big')
             else:
                 raise ValueError("Unknown encoding " + str(enc))
-            return data
+            return BV(size, n)
         else:
             raise ValueError("Unknown expression tag " + tag)
     else: