python .result() type information

[weaversa]

In an effort to maintain type information regarding the size of returned elements, consider returning Python BitVectors (maybe a .resultBV() or something that returns a BitVector or a sequence of BitVectors depending on the result type). This would remove the need for some munging between calls.

Imagine I have a function F that returns a sequence of, say, 5-bit values, and I need to pass those values to another function.

bits_5 = c.call("F", myvalues)
result = c.call("G", [BitVector(size=5, intVal = ord(e)) for e in bits_5.result()])

if resultBV() (or whatever) gave properly types BitVectors, I could instead write:

result = c.call("G", c.call("F", myvalues).resultBV())

[weaversa]

Or, is there already a way to pass results to a call? Does the Python client's call accept JSON Cryptol expressions as arguments? It does not.

[pnwamk]

I looked into this and chatted a little with @david-christiansen and was wondering if it wouldn't be better for result() to just return a convenient and non-lossy kind of value instead of python's native bytes (since they have no notion of the original value's width as you noted).

I made some progress today playing with a Bits python class which would take a bit-width and integer value as arguments and would allow you to perform a variety of natural/useful operations that would be helpful for working with Cryptol and allow for interoperation with native python values when it makes sense, e.g.:

>>> from bits import Bits
>>> b255 = Bits(8, 255)
>>> b255
Bits(8, 0xff)
>>> b255 + 1
Bits(8, 0x00)
>>> b255 + Bits(8, 0x2)
Bits(8, 0x01)
>>> b255[0:4]
Bits(4, 0xf)

(I initially started looking at using BitVector for this canonical return value, but the more I dug into that class the less convinced I became it was a good fit for representing and working with Cryptol bit sequences.)

Anyway, let me know if this sounds problematic or anything for how you're using the API.

[weaversa]

After trying BitVector I'm also not convinced they are that great here. What you have above seems pretty good. Here's a list of bitvector functions I've found useful for representing Cryptol-ish things - https://github.com/weaversa/bitvector/blob/master/src/bitvector.c

I'd love to test out what you have.

[pnwamk]

I should have a version posted sometime today.

[pnwamk]

Well today I implemented a Bits class and tested its basic behavior. I'll have to hook it up to the Cryptol API and test that aspect tomorrow (I took a stab but there's some probably silly bug in the way and it's getting late here).

[pnwamk]

This cryptol branch has the appropriate submodule bump to use the first draft of the new class for bit sequences (now called BV): https://github.com/GaloisInc/cryptol/tree/cryptol-bits-as-BV

There is no long-form documentation as of yet. I tried to document each member function where applicable; for now the test suite is likely useful to glance at for currently supported operations and behavior details.

[pnwamk]

I believe this issue is mostly solved with our switch to BV as the canonically returned python value for sequences of bits (see https://github.com/GaloisInc/argo/commit/ca97f5ab5413238da061ab076ccfb5895cb56ae4). If I missed an aspect that still needs addressing please let me know! =)