Improve the UX of the Python API

[chameco]

In order to make working with SAW more accessible, we would like the SAW Python API to be a viable alternative to SAWScript. The Python API is already near feature parity with the SAWScript interface for typical LLVM verification tasks. However, my impression is that there is still a gap in user experience between the two interfaces. The Python interface is not yet "first class" in the way that SAWScript is - we should strive to bridge this gap in usability.

In particular:

• Manipulation of terms is more unwieldy in the Python API. From my perspective, one of the unique strengths of the SAWScript interface is its tight integration with Cryptol. Beyond merely importing Cryptol specifications, there is syntax to easily write Cryptol expressions inline, and these expressions may in turn reference SAW Terms seamlessly. The ability to easily use Cryptol as a "glue" language in this way while writing specs informs the design of other parts of the SAWScript interface. There's some cool infrastructure on the Python side that makes this easier in some common cases (notably [RPC] Update with latest cryptol_client, fix types #1550), but there's space to do more - I think Python bindings: Make Cryptol quasiquotation easier #1188 has some good discussion on related topics. It's possible that the most ergonomic interface in Python looks significantly different compared to SAWScript, which raises other questions related to a potential automatic SAWScript -> Python translator.
• Interactive mode is clunkier in Python. I often find myself opening a SAW REPL to run :env, check the type of some command, eval_int some Cryptol, or inspect a Term. The subshell command introduced in Proof development primitives #1637 is a powerful tool that makes it much easier to enter the REPL within the context of a larger proof. In general I see a trend toward more interactive use of SAW during development. We should make sure that the interactive experience in Python is good, and that similar tools are available in that setting.
• Proof debugging is more difficult in Python. In my experience, a large part of debugging a SAW proof has involved doing "print-statement debugging" on the Haskell codebase (for better or for worse). Often, the easiest way to diagnose an issue is to print a term mid-command, or print some internal state, or print every address that the symbolic simulator tries to read, etc. Sometimes this involves adding temporary top-level or proofscript commands to the SAWScript interpreter. Although I haven't played around with it very much, my feeling is that the Python interface impedes this process by involving additional "stuff" - suddenly there are twice as many proceeses and a JSONRPC server involved. I think the root of the problem is that this sort of low-level interaction with the source code of the tool is the easiest (or only!) way to obtain certain useful information, and improving this situation would be very nice for SAWScript as well.
  @andreistefanescu and I have brainstormed a few ideas related to this in the past (better use of verbosity levels in error messages, maybe named breakpoints to identify particular places to enable printing, maybe ways to easily drop into GHCi or another interactive interface), and I'm sure that there's an endless amount of design that could be done in this space.

@m-yac @RyanGlScott I think you've worked with the Python interface more than I have, so I'd especially appreciate any thoughts you might have re: things we could do to make it better, or if any of the above is totally off-base.

[RyanGlScott]

Manipulation of [Cryptol] terms is more unwieldy in the Python API

To be honest, I haven't really tried using embedded Cryptol terms with cry_f after #1550. My impression was that cry_f bridged the gap between SAW and Python here. If not, what discrepancies still remain? I see that #1188 is still open, but it's unclear to me what the current status of that issue is now that #1550 has landed.

Interactive mode is clunkier in Python

Yes, I think we could go even further to enhance the experience of the SAW client in a Python REPL. That being said, some SAW commands won't cleanly translate over to Python. For example, SAW type signatures and Python type signatures look rather different, so a Python equivalent of SAW's :env command would have to do something else. Perhaps it should print the function signatures as they appear in the docstrings, much like what pydoc.doc() shows.

Having a Python equivalent of subshell would also be nifty.

Proof debugging is more difficult in Python

I'd go even further and say that proof debugging is difficult in SAW, period. I don't really have any grand ideas myself for making this easier, although I hope that subshell would be a step towards making things easier.

[chameco]

If not, what discrepancies still remain?

cry_f in particular produces a SetupVal, and can therefore get a bit messy in other places you might want a Term(for example, in prove). Generally, things that would take a Term in SAWScript (I think only the prove and save term commands are currently implemented) accept a Cryptol Expression in Python, which will make using non-Cryptol terms a bit more verbose. I believe the only such terms currently manipulated within the remote API are fresh variables within the context of a Crucible specification, but in the future we might want to support things like e.g. parse_core, llvm_compositional_extract, or rewrite. I think a lot of the machinery to handle these nicely already exists within the SetupVal class hierarchy - we might want to move some of that to a more general Term type and then use a separate type for Crucible memory layout, mirroring the way it works in SAWScript.

The above aren't really "limitations", as I think all of the tools we need are already exposed by the RPC server, but more just quirks of the interface that it would be nice to think about going forward.

I'd go even further and say that proof debugging is difficult in SAW, period.

100% agreed. I think improving the debugging experience is one of the most useful/important things that we can do for SAW, and I want to make sure the Python interface isn't left behind by any improvements in that area.

Unrelatedly, it struck me that an effective way of "dogfooding" the remote API might be to factor the SAWScript interpreter itself out as another RPC client. Maybe this is too cumbersome right now though (if so, we should think about why!).