Python string support for Cryptol interface

[pnwamk]

What should a Python string value be interpreted as by the Cryptol frontend (if anything)?

Discussion began here: #116

Current user experience with the Python-Cryptol API suggests it would be convenient to have some reasonable support for string literals, e.g., perhaps interpreting them as a sequence of ASCII bytes or similar (i.e., a cryptol [n][8] where n is the length of the ASCII string).

Background

At the moment the Python-Cryptol API does not convert string values to cryptol values, but historically in Cryptol (i.e., according to the docs strings have been supported. Specifically, in section 1.10 "Characters and strings", it explains strings are a form of syntactic sugar for byte sequences:

Strictly speaking Cryptol does not have characters and strings as a separate type. 
However, Cryptol does allow characters in programs, which simply correspond to 
their ASCII equivalents. Similarly, strings are merely sequences of characters,
i.e., sequences of words. The following examples illustrate:

Cryptol> :set base=10
Cryptol> :set ascii=off
Cryptol> 'A'
65
Cryptol> "ABC"
[65, 66, 67]
Cryptol> :set ascii=on
Cryptol> "ABC"
"ABC"
Cryptol> :set ascii=off
Cryptol> ['A' .. 'Z']
[65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79,
80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90]
Cryptol> :set ascii=on
Cryptol> ['A' .. 'Z']
"ABCDEFGHIJKLMNOPQRSTUVWXYZ

However, the implementation of Cryptol has been more permissive than suggested in the quoted section, e.g.:

Cryptol> "ø"
[0xf8]

Note that "ø" is not an ASCII-representable string, but is accepted as a valid string-literal by Cryptol currently.

Related issue: polymorphic string literals in Cryptol

There is a proposal for Cryptol strings to---like decimal literals---be polymorphic and have their meaning inferred by context: GaloisInc/cryptol#864. E.g., this would allow a string literal in to be treated as an ASCII string one context and as a UTF-8 string in the other.

Possibly related issue: Python-Cryptol API conversion of bytes

The Python-Cryptol API does currently convert python bytes values into Cryptol values: it converts them into a BV value in Python which represents a single sequence of bits in Cryptol. However, after thinking about strings more, I'm wondering if it wouldn't make more sense for our treatment of python str and bytes values to be somewhat consistent. E.g., would it make more sense for a bytes to be converted into a sequence of byte values instead of into a single sequence of bits? This is obviously a separate issue but I think it's worth considering our consistency here if we think that is relevant.

[pnwamk]

Another related (cryptol but non-python interface per se) issue: GaloisInc/cryptol#863

[david-christiansen]

WRT strings, I think that we should wait until GaloisInc/cryptol#864 is merged in its final form, and then provide a server-side feature for translating strings rather than a client-side one. This makes sure we get the same behavior.

[pnwamk]

I like that idea a lot! So we can basically just allow clients to send a "string" type for string values and then leave sane/sound reasoning about "string" values to Cryptol itself =)

[weaversa]

would it make more sense for a bytes to be converted into a sequence of byte values instead of into a single sequence of bits?

Passing "mystring".encode() to cryptol.call() becomes 64-bits rather than 8-bytes. Which is not what I would want. I suggest Python bytes be converted into a sequence of 8-bit bitvectors, and folks can use bitvector.py (which provides join and split operators) if they need to reshape data.