[RPC] Synchronous, typed interface for Python client

[m-yac]

This PR adds a synchronous and type-annotated interface for the python Cryptol RPC bindings. The advantages of such an interface are:

• No more calls to .result(), since everything is synchronous
• mypy can give useful feedback about the results of running RPC commands, since everything is type-annotated (for example, the return type of check is annotated to be a CheckResult)

All the tests have been updated to use the new interface, though the old interface still exists and is functionally unchanged (aside from the one exception noted below).

This PR also makes the following two changes that affect both the old and new interfaces:

• The CheckReport class now has __bool__ method which returns the value of its success field (e.g. so self.assert(c.check(...).success) can be replaced with just self.assert(c.check(...))).
• Instead of returning a Union[bool, List[CryptolPython], OfflineSmt], the sat, prove, and safe methods now return a Union[SmtResult, OfflineSmtQuery], where SmtResult has the subclasses SmtUnsatResult, SmtSatResult, and SmtInvalidResult. The SmtUnsatResult class has a __bool__ method which corresponds to the old bool case and the SmtSatResult and SmtInvalidResult classes are subclasses of List[CryptolPython]. Thus, this change will only break code which explicitly checks whether the result of sat/prove/safe is a bool (e.g. isinstance(c.sat(...).result(), bool)) but not code which just uses it as a truthy value (e.g. if c.sat(...).result(): ...).

Question: I called the type of the output of from_cryptol_arg "CryptolPython", but I feel like this could potentially be confusing. Thoughts on a better name?

NB: The definition of CryptolPython really should be:

CryptolPython = Union[bool, int, BV, Tuple[CryptolPython], List[CryptolPython], Dict[str, CryptolPython], OpaqueValue]

but mypy doesn't yet support recursive types.

[atomb]

This looks nice. As I mentioned in a comment, maybe CryptolValue would be a good name for what you're currently calling CryptolType? Although maybe that would make people think that it's for the Cryptol syntax of values, rather than the Python interpretation of them.

[pnwamk]

Love the changes. Just have some minor comments here and there, possibly bikeshedding on the interface of the SMT-related commands xD (sorry - I got confused and thought maybe a slightly simpler set of return types would help).

[pnwamk]

Tell me what you think! It seems like having to worry about whether or not we got an OfflineSmtQuery in every instance where we call one of these functions is silly, because we can only get those under certain circumstances. I.e., when the solver is specified as an offline solver. Would it be nice to have prove_offline, sat_offline, and check_offline which only returns a OfflineSmtQuery?

We could then be clearer about our SMT Solver type (I forget what it's called as I'm typing this), and have one type for the online solvers (probably called whatever it is now), and then have a specific OfflineSolver type that delineates the available offline solvers. Then the online and offline versions of the functions could be specific about what solvers they allow, and the return types could not worry about the impossible result types! (i.e., online query will never return OfflineSmtQuery, etc).

Aye? Thoughts?

[m-yac]

In the spirit of having the Python interface mirror the REPL interface, I didn't make separate methods for offline queries, I instead used @overloads to give the two cases (the OnlineSolver and OfflineSolver cases, as I called them) distinct types. Let me know what you think

[pnwamk]

Do these functions need the _sync prefix, given that they're in their own module? (i.e., if you wanted to import the old and new interface, couldn't you have a prefix on the module imports to tell them apart?)

It's not a big deal, but it seems like if we move towards having the synchronous interface be the default it might be funny to have _sync on the methods. If anything we'd want the default interface to be smooth/streamlined and the odd one to have warts (if it has to -- i.e., if import prefixes aren't sufficient).

(Maybe I'm not seeing a reason to have the suffixes though?)

[m-yac]

I refactored so now the tests use cryptol.sync.connect(...) instead of cryptol.connect_sync(...). I don't know if the module trickery I did to get sync working as an abbreviation is very Pythonic though... see __init__.py

[m-yac]

Looks like the CI failures have nothing to do with these RPC changes.

@pnwamk pinging you to see if you want to take another look at this to make sure I addressed your comments.

[pnwamk]

LGTM modulo adding just a tiny more to the docstrings of those SMT-related queries IMO.

[m-yac]

LGTM modulo adding just a tiny more to the docstrings of those SMT-related queries IMO.

Good catch, adding docs for this is important. What do you think of my latest commit?

[pnwamk]

LGTM

On Wed, Sep 15, 2021 at 13:54 Matthew Yacavone ***@***.***> wrote: LGTM modulo adding just a tiny more to the docstrings of those SMT-related queries IMO. Good catch, adding docs for this is important. What do you think of my latest commit? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1272 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA36B2RUUB52B7U5ZTYD4YDUCEB2BANCNFSM5C6GPHJQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

-- *Andrew M. Kent, PhD* *Research Engineer* *Galois, Inc.*