From af8fbe01aa87efc1d35b15ea0227a97293a70b52 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Wed, 1 Dec 2021 12:18:41 -0800
Subject: [PATCH 1/9] WIP on quoted cryptol in SAW python

---
 deps/cryptol                                  |  2 +-
 saw-remote-api/python/poetry.lock             | 24 +++---
 saw-remote-api/python/pyproject.toml          |  2 +-
 saw-remote-api/python/saw_client/crucible.py  | 38 ++++++----
 .../python/tests/saw-in-progress/drbg/drbg.py | 76 +++++++++----------
 .../python/tests/saw/test_alloc_aligned.py    |  4 +-
 .../python/tests/saw/test_basic_java.py       |  6 +-
 saw-remote-api/python/tests/saw/test_ghost.py | 10 +--
 .../python/tests/saw/test_llvm_assert_null.py |  6 +-
 .../python/tests/saw/test_llvm_pointer.py     |  4 +-
 .../python/tests/saw/test_llvm_struct.py      |  6 +-
 .../python/tests/saw/test_llvm_struct_type.py |  4 +-
 .../tests/saw/test_points_to_at_type.py       |  4 +-
 .../python/tests/saw/test_salsa20.py          | 28 +++----
 14 files changed, 109 insertions(+), 105 deletions(-)

diff --git a/deps/cryptol b/deps/cryptol
index cffdcdd049..abb41f5b4e 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit cffdcdd04963e11c60d8a234b297c02a7e5a06ca
+Subproject commit abb41f5b4e16bfc351ec6c6a6a419c36fd94ac10
diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock
index 9e42ce7fb7..f91ca9d35f 100644
--- a/saw-remote-api/python/poetry.lock
+++ b/saw-remote-api/python/poetry.lock
@@ -28,7 +28,7 @@ python-versions = "*"
 
 [[package]]
 name = "charset-normalizer"
-version = "2.0.7"
+version = "2.0.8"
 description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet."
 category = "main"
 optional = false
@@ -39,16 +39,21 @@ unicode_backport = ["unicodedata2"]
 
 [[package]]
 name = "cryptol"
-version = "2.12.0"
+version = "2.12.1"
 description = "Cryptol client for the Cryptol 2.12 RPC server"
 category = "main"
 optional = false
 python-versions = ">=3.7.0"
+develop = true
 
 [package.dependencies]
 argo-client = "0.0.9"
-BitVector = ">=3.4.9,<4.0.0"
-requests = ">=2.25.1,<3.0.0"
+BitVector = "^3.4.9"
+requests = "^2.25.1"
+
+[package.source]
+type = "directory"
+url = "../../deps/cryptol/cryptol-remote-api/python"
 
 [[package]]
 name = "idna"
@@ -132,7 +137,7 @@ socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"]
 [metadata]
 lock-version = "1.1"
 python-versions = "^3.8"
-content-hash = "2e8d483be348117d70d8a2683748a807483cb4fba322c2be61dfe826bd7ef9fd"
+content-hash = "d1ec6c507e7a1f0f935f625feec468b2291974cc537e2891f1f0bbfcc70416bb"
 
 [metadata.files]
 argo-client = [
@@ -147,13 +152,10 @@ certifi = [
     {file = "certifi-2021.10.8.tar.gz", hash = "sha256:78884e7c1d4b00ce3cea67b44566851c4343c120abd683433ce934a68ea58872"},
 ]
 charset-normalizer = [
-    {file = "charset-normalizer-2.0.7.tar.gz", hash = "sha256:e019de665e2bcf9c2b64e2e5aa025fa991da8720daa3c1138cadd2fd1856aed0"},
-    {file = "charset_normalizer-2.0.7-py3-none-any.whl", hash = "sha256:f7af805c321bfa1ce6714c51f254e0d5bb5e5834039bc17db7ebe3a4cec9492b"},
-]
-cryptol = [
-    {file = "cryptol-2.12.0-py3-none-any.whl", hash = "sha256:32230c361f79bfd621c7c7872d338c8e315d55c368c38730fa792d4626321204"},
-    {file = "cryptol-2.12.0.tar.gz", hash = "sha256:bedde0bc55fff411bfd9575b5fd77890ce855a921340d2e805453c64fbae652e"},
+    {file = "charset-normalizer-2.0.8.tar.gz", hash = "sha256:735e240d9a8506778cd7a453d97e817e536bb1fc29f4f6961ce297b9c7a917b0"},
+    {file = "charset_normalizer-2.0.8-py3-none-any.whl", hash = "sha256:83fcdeb225499d6344c8f7f34684c2981270beacc32ede2e669e94f7fa544405"},
 ]
+cryptol = []
 idna = [
     {file = "idna-3.3-py3-none-any.whl", hash = "sha256:84d9dd047ffa80596e0f246e2eab0b391788b0503584e8945f2368256d2735ff"},
     {file = "idna-3.3.tar.gz", hash = "sha256:9d643ff0a55b762d5cdb124b8eaa99c66322e2157b69160bc32796e824360e6d"},
diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml
index a5c8c0dae4..86f8ce85ae 100644
--- a/saw-remote-api/python/pyproject.toml
+++ b/saw-remote-api/python/pyproject.toml
@@ -14,7 +14,7 @@ include = [
 python = "^3.8"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-cryptol = "2.12.0" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
+cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
 argo-client = "~0.0.6"
 
 [tool.poetry.dev-dependencies]
diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index f17ae1057d..a4ecea079e 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -1,5 +1,6 @@
 from abc import ABCMeta, abstractmethod
 from cryptol import cryptoltypes
+from cryptol.quoting import to_cryptol_str_customf
 from .utils import deprecated
 from dataclasses import dataclass
 import dataclasses
@@ -81,9 +82,12 @@ def __repr__(self) -> str:
     def to_json(self) -> Any:
         return {'setup value': 'Cryptol', 'expression': cryptoltypes.to_cryptol(self.expression)}
 
-    def __to_cryptol__(self, ty : Any) -> Any:
+    def __to_cryptol__(self, ty : Any) -> cryptoltypes.JSON:
         return self.expression.__to_cryptol__(ty)
 
+    def __to_cryptol_str__(self) -> str:
+        return self.expression.__to_cryptol_str__()
+
 class FreshVar(NamedSetupVal):
     __name : Optional[str]
 
@@ -92,9 +96,12 @@ def __init__(self, spec : 'Contract', type : Union['LLVMType', 'JVMType'], sugge
         self.spec = spec
         self.type = type
 
-    def __to_cryptol__(self, ty : Any) -> Any:
+    def __to_cryptol__(self, ty : Any) -> cryptoltypes.JSON:
         return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__(ty)
 
+    def __to_cryptol_str__(self) -> str:
+        return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol_str__()
+
     def to_init_json(self) -> Any:
         #FIXME it seems we don't actually use two names ever... just the one...do we actually need both?
         name = self.name()
@@ -567,18 +574,21 @@ def to_json(self) -> Any:
 
 # It's tempting to name this `global` to mirror SAWScript's `llvm_global`,
 # but that would clash with the Python keyword `global`.
-def global_var(name: str) -> SetupVal:
+def global_var(name: str) -> GlobalVarVal:
     """Returns a pointer to the named global ``name`` (i.e., a ``GlobalVarVal``)."""
     return GlobalVarVal(name)
 
-# FIXME Is `Any` too permissive here -- can we be a little more precise?
-def cryptol(data : Any) -> 'CryptolTerm':
-    """Constructs a Cryptol value from ``data`` (i.e., a ``CryptolTerm``, which is also a ``SetupVal``).
+def cry(s : str) -> CryptolTerm:
+    """Like ``cry`` from the Cryptol bindings, but retuns a ``CryptolTerm``
+    (which is also a ``SetupVal``)."""
+    return CryptolTerm(s)
 
-    ``data`` should be a string literal representing Cryptol syntax or the result of a Cryptol-realted server computation."""
-    return CryptolTerm(data)
+def cry_f(s : str) -> CryptolTerm:
+    """Like ``cry_f`` from the Cryptol bindings, but retuns a ``CryptolTerm``
+    (which is also a ``SetupVal``)."""
+    return CryptolTerm(to_cryptol_str_customf(s, frames=1, filename='<cryptol_f>'))
 
-def array(*elements: SetupVal) -> SetupVal:
+def array(*elements: SetupVal) -> ArrayVal:
     """Returns an array with the provided ``elements`` (i.e., an ``ArrayVal``).
 
     N.B., one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out.
@@ -589,7 +599,7 @@ def array(*elements: SetupVal) -> SetupVal:
             raise ValueError('array expected a SetupVal, but got {e!r}')
     return ArrayVal(list(elements))
 
-def elem(base: SetupVal, index: int) -> SetupVal:
+def elem(base: SetupVal, index: int) -> ElemVal:
     """Returns the value of the array element at position ``index`` in ``base`` (i.e., an ``ElemVal``).
 
     Can also be created by using an ``int`` indexing key on a ``SetupVal``: ``base[index]``."""
@@ -599,7 +609,7 @@ def elem(base: SetupVal, index: int) -> SetupVal:
         raise ValueError('elem expected an int, but got {index!r}')
     return ElemVal(base, index)
 
-def field(base : SetupVal, field_name : str) -> SetupVal:
+def field(base : SetupVal, field_name : str) -> FieldVal:
     """Returns the value of struct ``base``'s field ``field_name`` (i.e., a ``FieldVal``).
 
     Can also be created by using a ``str`` indexing key on a ``SetupVal``: ``base[field_name]``."""
@@ -609,17 +619,17 @@ def field(base : SetupVal, field_name : str) -> SetupVal:
         raise ValueError('field expected a str, but got {field_name!r}')
     return FieldVal(base, field_name)
 
-def global_initializer(name: str) -> SetupVal:
+def global_initializer(name: str) -> GlobalInitializerVal:
     """Returns the initializer value of a named global ``name`` (i.e., a ``GlobalInitializerVal``)."""
     if not isinstance(name, str):
         raise ValueError('global_initializer expected a str naming a global value, but got {name!r}')
     return GlobalInitializerVal(name)
 
-def null() -> SetupVal:
+def null() -> NullVal:
     """Returns a null pointer value (i.e., a ``NullVal``)."""
     return NullVal()
 
-def struct(*fields : SetupVal) -> SetupVal:
+def struct(*fields : SetupVal) -> StructVal:
     """Returns an LLVM structure value with the given ``fields`` (i.e., a ``StructVal``)."""
     for field in fields:
         if not isinstance(field, SetupVal):
diff --git a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
index a97cbe4465..78c6a03b65 100755
--- a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
+++ b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
@@ -39,16 +39,16 @@ def alloc_blob(spec, n):
     p = spec.alloc(type=blob_type, read_only=True)
     datap = alloc_bytes(spec, n)
     spec.points_to(llvm.field(p, "data"), datap)
-    spec.points_to(llvm.field(p, "size"), llvm.cryptol("`{n}:[32]".format(n=n)))
-    spec.points_to(llvm.field(p, "allocated"), llvm.cryptol("0:[32]"))
-    spec.points_to(llvm.field(p, "growable"), llvm.cryptol("0:[8]"))
+    spec.points_to(llvm.field(p, "size"), llvm.cry_f("`{n}:[32]"))
+    spec.points_to(llvm.field(p, "allocated"), llvm.cry("0:[32]"))
+    spec.points_to(llvm.field(p, "growable"), llvm.cry("0:[8]"))
     return (p, datap)
 
 def alloc_blob_readonly(spec, n):
     p = spec.alloc(type=blob_type, read_only=True)
     datap = spec.alloc(llvm_types.array(n, llvm_types.i8), read_only = True)
     spec.points_to(llvm.field(p, "data"), datap)
-    spec.points_to(llvm.field(p, "size"), llvm.cryptol("`{n}: [32]".format(n=n)))
+    spec.points_to(llvm.field(p, "size"), llvm.cry_f("`{n}: [32]"))
     return(p, datap)
 
 def alloc_init(spec, ty, v):
@@ -86,16 +86,8 @@ def drbg_state(spec, n):
     spec.points_to(llvm.field(state, "mixes"), mixes)
     spec.points_to(llvm.field(state, "ctx"), keyp)
     spec.points_to(llvm.field(state, "v"), v)
-    return (state, keyp,
-            "{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}".format(bytes_used=bytes_used.name(), key=key.name(), v=v.name()))
-    #return (state, keyp,
-    #        llvm.cryptol("{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}".format(bytes_used=bytes_used.name(), key=key.name(), v=v.name())))
-    #return (state, keyp, { 'bytes_used': bytes_used , 'ctx': { 'key': llvm.cryptol("join {}".format(key.name())) } , v: llvm.cryptol("join {}".format(v)) })
+    return (state, keyp, cry_f("{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}"))
 
-    #       , {{ { bytes_used = bytes_used
-    #           , ctx = { key = join key }
-    #           , v = join v
-    #           } }}
 
 class blob_zero_spec(Contract):
     def __init__(self,n):
@@ -105,8 +97,8 @@ def __init__(self,n):
     def specification(self):
         (p, datap) = alloc_blob(self, self.n)
         self.execute_func(p)
-        self.points_to(datap, llvm.cryptol("zero:[{n}][8]".format(n=self.n)))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.points_to(datap, llvm.cry("zero:[{n}][8]".format(n=self.n)))
+        self.returns(llvm.cry("0:[32]"))
 
 class increment_drbg_counter_spec(Contract):
     def specification(self):
@@ -114,16 +106,16 @@ def specification(self):
         v = self.fresh_var(bytes_type(blocksize), "v")
         self.points_to(datap, v)
         self.execute_func(p)
-        self.points_to(datap, llvm.cryptol("split ((join {v}) +1): [{blocksize}][8]".format(v=v.name(),blocksize=blocksize)))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.points_to(datap, llvm.cry("split ((join {v}) +1): [{blocksize}][8]".format(v=v.name(),blocksize=blocksize)))
+        self.returns(llvm.cry("0:[32]"))
 
 class bytes_used_spec(Contract):
     def specification(self):
         (sp, keyp, s) = drbg_state(self,"drbg")
-        bytes_used = alloc_init(self, llvm_types.i64, llvm.cryptol("0:[64]"))
+        bytes_used = alloc_init(self, llvm_types.i64, llvm.cry("0:[64]"))
         self.execute_func(sp, bytes_used)
-        self.points_to(bytes_used, llvm.cryptol("{s}.bytes_used".format(s=s)))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.points_to(bytes_used, llvm.cry_f("{s}.bytes_used"))
+        self.returns(llvm.cry("0:[32]"))
 
 class block_encrypt_spec(Contract):
     def specification(self):
@@ -131,8 +123,8 @@ def specification(self):
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", bytes_type(blocksize))
         outp = alloc_bytes(self, blocksize)
         self.execute_func(keyp, msgp, outp)
-        self.points_to(outp, llvm.cryptol("encrypt_128 {key} {msg}".format(key=key.name(), msg=msg.name())))
-        self.returns(llvm.cryptol("0 : [32]"))
+        self.points_to(outp, llvm.cry("encrypt_128 {key} {msg}".format(key=key.name(), msg=msg.name())))
+        self.returns(llvm.cry("0 : [32]"))
 
 class encryptUpdate_spec(Contract):
     def __init__(self,n):
@@ -143,12 +135,12 @@ def specification(self):
         # but it is constant in the DRBG cryptol specification.
         (key, keyp) = ptr_to_fresh_readonly(self, "key", ctx_type)
         outp = alloc_bytes(self, self.n)
-        lenp = alloc_init(self, llvm_types.i32, llvm.cryptol("{} : [32]".format(self.n)))
+        lenp = alloc_init(self, llvm_types.i32, llvm.cry("{} : [32]".format(self.n)))
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", (bytes_type(self.n)))
-        self.execute_func(keyp, outp, lenp, msgp, llvm.cryptol("`{blocksize} : [32]".format(blocksize=blocksize)))
-        self.points_to(outp, llvm.cryptol("encrypt_128 {} {}".format(key.name(), msg.name())))
-        self.points_to(lenp, llvm.cryptol("{} : [32]".format(self.n)))
-        self.returns (llvm.cryptol("1 : [32]"))
+        self.execute_func(keyp, outp, lenp, msgp, llvm.cry("`{blocksize} : [32]".format(blocksize=blocksize)))
+        self.points_to(outp, llvm.cry("encrypt_128 {} {}".format(key.name(), msg.name())))
+        self.points_to(lenp, llvm.cry("{} : [32]".format(self.n)))
+        self.returns (llvm.cry("1 : [32]"))
 
 class bits_spec(Contract):
     def __init__(self, n):
@@ -158,18 +150,18 @@ def specification(self):
         (sp, keyp, s) = drbg_state(self, "drbg")
         (outp, datap) = alloc_blob(self, self.n)
         self.execute_func(sp, outp)
-        res = "drbg_generate_internal `{{n={n}*8}} ({s})".format(n=self.n,s=s)
+        res = cry_f("drbg_generate_internal `{{n={self.n}*8}} {s}")
         # Remove some of the parens here to get really bad error messages
-        c = llvm.cryptol("split (({res}).0) : [{n}][8]".format(res=res, n=self.n))
+        c = llvm.cry("split (({res}).0) : [{n}][8]".format(res=res, n=self.n))
         self.points_to(datap, c)
-        ensure_drbg_state(self, sp, keyp, "({res}).1".format(res=res))
-        self.returns (llvm.cryptol(" 0 : [32] "))
+        ensure_drbg_state(self, sp, keyp, cry_f("{res}.1"))
+        self.returns (llvm.cry(" 0 : [32] "))
 
 def ensure_drbg_state(spec, p, keyp, s):
-    spec.points_to(llvm.field(p, "bytes_used"), llvm.cryptol("({s}).bytes_used".format(s=s)))
+    spec.points_to(llvm.field(p, "bytes_used"), llvm.cry("({s}).bytes_used".format(s=s)))
     spec.points_to(llvm.field(p, "ctx"), keyp)
-    spec.points_to(keyp, llvm.cryptol("split (({s}).ctx.key) : [{keysize}][8]".format(s=s,keysize=keysize)))
-    spec.points_to(llvm.field(p, "v"), llvm.cryptol("split (({s}).v) : [{blocksize}][8]".format(s=s,blocksize=blocksize)))
+    spec.points_to(keyp, llvm.cry("split (({s}).ctx.key) : [{keysize}][8]".format(s=s,keysize=keysize)))
+    spec.points_to(llvm.field(p, "v"), llvm.cry("split (({s}).v) : [{blocksize}][8]".format(s=s,blocksize=blocksize)))
     mixes = spec.fresh_var(llvm_types.i64, "mixes")
     spec.points_to(llvm.field(p, "mixes"), mixes)
 
@@ -212,15 +204,15 @@ class cipher_cleanup_spec(Contract):
     def specification(self):
         ctx = self.alloc(ctx_type)
         self.execute_func(ctx)
-        self.points_to(ctx, llvm.cryptol("zero : [{keysize}][8]".format(keysize=keysize)))
-        self.returns(llvm.cryptol("1:[32]"))
+        self.points_to(ctx, llvm.cry("zero : [{keysize}][8]".format(keysize=keysize)))
+        self.returns(llvm.cry("1:[32]"))
 
 class cipher_key_length_spec(Contract):
     def specification(self):
         ctx = self.alloc(ctx_type, read_only = True)
         self.execute_func(ctx)
         # Specialized to AES-128 for now
-        self.returns(llvm.cryptol("16:[32]"))
+        self.returns(llvm.cry("16:[32]"))
 
 class encryptInit_spec(Contract):
     def specification(self):
@@ -233,7 +225,7 @@ def specification(self):
         #self.execute_func(ctx, stp, llvm.null, keyp, llvm.null)
         self.execute_func(ctx, llvm.null, llvm.null, keyp, llvm.null)
         self.points_to(ctx, key)
-        self.returns(llvm.cryptol("1:[32]"))
+        self.returns(llvm.cry("1:[32]"))
 
 class get_public_random_spec(Contract):
     def __init__(self):
@@ -243,8 +235,8 @@ def specification(self):
         (p, datap) = alloc_blob(self, seedsize)
         self.execute_func(p)
         # TODO: blocked on 'fake_entropy'
-        #self.points_to(datap, llvm.cryptol("split fake_entropy : [{seedsize}][8]".format(seedsize=seedsize)))
-        self.returns(llvm.cryptol("0: [32]"))
+        #self.points_to(datap, llvm.cry("split fake_entropy : [{seedsize}][8]".format(seedsize=seedsize)))
+        self.returns(llvm.cry("0: [32]"))
 
 class supports_rdrand_spec(Contract):
     def specification(self):
@@ -283,7 +275,7 @@ def specification(self):
         self.points_to(datap, data)
         self.execute_func(sp, providedp)
         ensure_drbg_state(self, sp, keyp, "drbg_update (join {data}) ({s})".format(data=data.name(), s=s))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.returns(llvm.cry("0:[32]"))
 
 class seed_spec(Contract):
     def __init__(self, n):
@@ -298,7 +290,7 @@ def specification(self):
         expr = "drbg_reseed ({s}) (fake_entropy) (join ({data}))".format(s=s,
                 data=data.name())
         ensure_drbg_state(self, sp, keyp, expr)
-        self.returns(llvm.cryptol("0:[32]"))
+        self.returns(llvm.cry("0:[32]"))
 
 zero_ov_block = llvm_verify(mod, 's2n_blob_zero', blob_zero_spec(blocksize))
 zero_ov_seed = llvm_verify(mod, "s2n_blob_zero", blob_zero_spec(seedsize))
diff --git a/saw-remote-api/python/tests/saw/test_alloc_aligned.py b/saw-remote-api/python/tests/saw/test_alloc_aligned.py
index a82212b21f..22e11360b2 100644
--- a/saw-remote-api/python/tests/saw/test_alloc_aligned.py
+++ b/saw-remote-api/python/tests/saw/test_alloc_aligned.py
@@ -1,7 +1,7 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, FreshVar, SetupVal, cryptol, struct, LLVMType, array_ty, i8, i64
+from saw_client.llvm import Contract, FreshVar, SetupVal, cry, cry_f, struct, LLVMType, array_ty, i8, i64
 from typing import Tuple
 
 
@@ -16,7 +16,7 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tu
 
 
 def int_to_64_cryptol(length: int):
-    return cryptol("`{i}:[64]".format(i=length))
+    return cry_f("`{length}:[64]")
 
 
 def buffer_type(length: int) -> LLVMType:
diff --git a/saw-remote-api/python/tests/saw/test_basic_java.py b/saw-remote-api/python/tests/saw/test_basic_java.py
index 066b78f0fe..0267006889 100644
--- a/saw-remote-api/python/tests/saw/test_basic_java.py
+++ b/saw-remote-api/python/tests/saw/test_basic_java.py
@@ -3,7 +3,7 @@
 
 import saw_client as saw
 
-from saw_client.jvm import Contract, java_int, cryptol
+from saw_client.jvm import Contract, java_int, cry, cry_f
 
 class Add(Contract):
     def __init__(self) -> None:
@@ -15,7 +15,7 @@ def specification(self) -> None:
 
         self.execute_func(x, y)
 
-        self.returns(cryptol("(+)")(x,y))
+        self.returns(cry_f("{x} + {y}"))
 
 class Double(Contract):
     def __init__(self) -> None:
@@ -26,7 +26,7 @@ def specification(self) -> None:
 
         self.execute_func(x)
 
-        self.returns(cryptol("(+)")(x,x))
+        self.returns(cry_f("{x} + {x}"))
 
 class AddTest(unittest.TestCase):
     def test_add(self):
diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py
index be831b47de..5bddda8fd5 100644
--- a/saw-remote-api/python/tests/saw/test_ghost.py
+++ b/saw-remote-api/python/tests/saw/test_ghost.py
@@ -1,17 +1,17 @@
 import saw_client as saw
-from saw_client.llvm import Contract, CryptolTerm, cryptol, void, i32, GhostVariable
+from saw_client.llvm import Contract, CryptolTerm, cry, cry_f, void, i32, GhostVariable
 
 import unittest
 from pathlib import Path
 
 def pre_counter(contract: Contract, counter: GhostVariable):
     n = contract.fresh_var(i32, "n")
-    contract.precondition(n < cryptol("128"))
+    contract.precondition(n < cry("128"))
     contract.ghost_value(counter, n)
     return n
 
 def post_counter(contract: Contract, counter: GhostVariable, n: CryptolTerm):
-    contract.ghost_value(counter, cryptol("(+)")(n, cryptol("1")))
+    contract.ghost_value(counter, cry_f("{n} + 1"))
 
 class GetAndIncrementContract(Contract):
     def __init__(self, counter: str) -> None:
@@ -32,10 +32,10 @@ def __init__(self, counter: str) -> None:
     def specification(self) -> None:
         n = pre_counter(self, self.counter)
         i = self.fresh_var(i32, "i")
-        self.precondition(i < cryptol("512"))
+        self.precondition(i < cry("512"))
         self.execute_func(i)
         post_counter(self, self.counter, n)
-        self.returns(cryptol("(*)")(i, n))
+        self.returns(cry_f("{i} * {n}"))
 
 class GhostTest(unittest.TestCase):
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
index 99b613612f..c56d21fa4f 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
@@ -1,7 +1,7 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cryptol, null, i32
+from saw_client.llvm import Contract, cry, cry_f, null, i32
 
 
 class FContract1(Contract):
@@ -10,14 +10,14 @@ def specification(self):
 
         self.execute_func(p)
 
-        self.returns(cryptol("0 : [32]"))
+        self.returns(cry("0 : [32]"))
 
 
 class FContract2(Contract):
     def specification(self):
         self.execute_func(null())
 
-        self.returns(cryptol("1 : [32]"))
+        self.returns(cry("1 : [32]"))
 
 
 class LLVMAssertNullTest(unittest.TestCase):
diff --git a/saw-remote-api/python/tests/saw/test_llvm_pointer.py b/saw-remote-api/python/tests/saw/test_llvm_pointer.py
index a1a80aabbd..01ccb9113f 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_pointer.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_pointer.py
@@ -1,7 +1,7 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cryptol, void, i8, ptr_ty
+from saw_client.llvm import Contract, cry, cry_f, void, i8, ptr_ty
 
 
 class FContract(Contract):
@@ -12,7 +12,7 @@ def specification(self):
 
         p = self.alloc(i8)
         self.points_to(x, p)
-        self.points_to(p, cryptol("42 : [8]"))
+        self.points_to(p, cry("42 : [8]"))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct.py b/saw-remote-api/python/tests/saw/test_llvm_struct.py
index ff583ea03d..03408bf8a1 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_struct.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_struct.py
@@ -1,7 +1,7 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, SetupVal, FreshVar, cryptol, struct, LLVMType, void, array_ty, i32, alias_ty
+from saw_client.llvm import Contract, SetupVal, FreshVar, cry, cry_f, struct, LLVMType, void, array_ty, i32, alias_ty
 
 
 def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]:
@@ -22,7 +22,7 @@ def specification(self):
         self.execute_func(p)
 
         self.points_to(p, struct(x_p))
-        self.points_to(x_p, cryptol('[0, 0] : [2][32]'))
+        self.points_to(x_p, cry('[0, 0] : [2][32]'))
         self.returns(void)
 
 
@@ -33,7 +33,7 @@ def specification(self):
 
         self.execute_func(p)
 
-        self.returns(cryptol(f'{x.name()}@0 + {x.name()}@1'))
+        self.returns(cry_f('{x}@0 + {x}@1'))
 
 
 class IdContract(Contract):
diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
index 86feb33502..8c552f474a 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
@@ -1,7 +1,7 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cryptol, struct, void, i32, array_ty, struct_ty
+from saw_client.llvm import Contract, cry, cry_f, struct, void, i32, array_ty, struct_ty
 
 
 class FContract(Contract):
@@ -12,7 +12,7 @@ def specification(self):
 
         self.execute_func(pw)
 
-        self.points_to(pw, struct(cryptol('zero:[2][4][32]')))
+        self.points_to(pw, struct(cry('zero:[2][4][32]')))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_points_to_at_type.py b/saw-remote-api/python/tests/saw/test_points_to_at_type.py
index 6991a31114..577250cfb8 100644
--- a/saw-remote-api/python/tests/saw/test_points_to_at_type.py
+++ b/saw-remote-api/python/tests/saw/test_points_to_at_type.py
@@ -2,7 +2,7 @@
 import unittest
 from saw_client import *
 from saw_client.exceptions import VerificationError
-from saw_client.llvm import Contract, LLVMType, PointerType, cryptol, void, i32, array_ty
+from saw_client.llvm import Contract, LLVMType, PointerType, cry, cry_f, void, i32, array_ty
 from typing import Union
 
 
@@ -18,7 +18,7 @@ def specification(self) -> None:
 
         self.execute_func(p)
 
-        self.points_to(p, cryptol("{x} # {x}".format(x=x.name())))
+        self.points_to(p, cry_f("{x} # {x}"))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py
index 45afeff63d..c20e8fb325 100644
--- a/saw-remote-api/python/tests/saw/test_salsa20.py
+++ b/saw-remote-api/python/tests/saw/test_salsa20.py
@@ -2,7 +2,7 @@
 import unittest
 from cryptol.cryptoltypes import to_cryptol
 from saw_client import *
-from saw_client.llvm import Contract, void, SetupVal, FreshVar, cryptol, i8, i32, LLVMType, LLVMArrayType
+from saw_client.llvm import Contract, void, SetupVal, FreshVar, cry, cry_f, i8, i32, LLVMType, LLVMArrayType
 from saw_client.proofscript import z3
 
 
@@ -23,7 +23,7 @@ def oneptr_update_func(c : Contract, ty : LLVMType, fn_name : str) -> None:
 
     c.execute_func(x_p)
 
-    c.points_to(x_p, cryptol(fn_name)(x))
+    c.points_to(x_p, cry(fn_name)(x))
     c.returns(void)
     return None
 
@@ -32,12 +32,12 @@ class RotlContract(Contract):
     def specification(self) -> None:
         value = self.fresh_var(i32, "value")
         shift = self.fresh_var(i32, "shift")
-        self.precondition(shift > cryptol("0"))
-        self.precondition(shift < cryptol("32"))
+        self.precondition(shift > cry("0"))
+        self.precondition(shift < cry("32"))
 
         self.execute_func(value, shift)
 
-        self.returns(cryptol("(<<<)")(value, shift))
+        self.returns(cry_f("{value} <<< {shift}"))
 
 
 
@@ -55,11 +55,11 @@ def specification(self) -> None:
 
         self.execute_func(y0_p, y1_p, y2_p, y3_p)
 
-        res = cryptol("quarterround")([y0, y1, y2, y3])
-        self.points_to(y0_p, cryptol("(@)")(res, cryptol("0")))
-        self.points_to(y1_p, cryptol("(@)")(res, cryptol("1")))
-        self.points_to(y2_p, cryptol("(@)")(res, cryptol("2")))
-        self.points_to(y3_p, cryptol("(@)")(res, cryptol("3")))
+        res = cry_f("quarterround {[y0, y1, y2, y3]}")
+        self.points_to(y0_p, cry_f("{res} @ 0"))
+        self.points_to(y1_p, cry_f("{res} @ 1"))
+        self.points_to(y2_p, cry_f("{res} @ 2"))
+        self.points_to(y3_p, cry_f("{res} @ 3"))
         self.returns(void)
 
 
@@ -102,7 +102,7 @@ def specification(self):
         self.execute_func(k_p, n_p, ks_p)
 
         self.returns(void)
-        self.points_to(ks_p, cryptol("Salsa20_expansion`{a=2}")((k, n)))
+        self.points_to(ks_p, cry_f("Salsa20_expansion`{{a=2}} {(k, n)}"))
 
 
 
@@ -116,10 +116,10 @@ def specification(self):
         (v, v_p) = ptr_to_fresh(self, LLVMArrayType(i8, 8))
         (m, m_p) = ptr_to_fresh(self, LLVMArrayType(i8, self.size))
 
-        self.execute_func(k_p, v_p, cryptol('0 : [32]'), m_p, cryptol(f'{self.size!r} : [32]'))
+        self.execute_func(k_p, v_p, cry('0 : [32]'), m_p, cry_f('{self.size} : [32]'))
 
-        self.points_to(m_p, cryptol("Salsa20_encrypt")((k, v, m)))
-        self.returns(cryptol('0 : [32]'))
+        self.points_to(m_p, cry_f("Salsa20_encrypt {(k, v, m)}"))
+        self.returns(cry('0 : [32]'))
 
 class Salsa20EasyTest(unittest.TestCase):
     def test_salsa20(self):

From 642b963540daab1dbda8b79e415f47c6ff43baf5 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 3 Dec 2021 12:23:07 -0800
Subject: [PATCH 2/9] finish using `cry_f` and `cry` in SAW python tests

---
 saw-remote-api/python/poetry.lock             |  6 ++---
 .../python/tests/saw-in-progress/drbg/drbg.py | 27 +++++++++----------
 .../python/tests/saw/test_salsa20.py          | 10 +++----
 3 files changed, 21 insertions(+), 22 deletions(-)

diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock
index f91ca9d35f..c4e4413bf6 100644
--- a/saw-remote-api/python/poetry.lock
+++ b/saw-remote-api/python/poetry.lock
@@ -115,7 +115,7 @@ python-versions = "*"
 
 [[package]]
 name = "typing-extensions"
-version = "4.0.0"
+version = "4.0.1"
 description = "Backported and Experimental Type Hints for Python 3.6+"
 category = "main"
 optional = false
@@ -225,8 +225,8 @@ typed-ast = [
     {file = "typed_ast-1.4.3.tar.gz", hash = "sha256:fb1bbeac803adea29cedd70781399c99138358c26d05fcbd23c13016b7f5ec65"},
 ]
 typing-extensions = [
-    {file = "typing_extensions-4.0.0-py3-none-any.whl", hash = "sha256:829704698b22e13ec9eaf959122315eabb370b0884400e9818334d8b677023d9"},
-    {file = "typing_extensions-4.0.0.tar.gz", hash = "sha256:2cdf80e4e04866a9b3689a51869016d36db0814d84b8d8a568d22781d45d27ed"},
+    {file = "typing_extensions-4.0.1-py3-none-any.whl", hash = "sha256:7f001e5ac290a0c0401508864c7ec868be4e701886d5b573a9528ed3973d9d3b"},
+    {file = "typing_extensions-4.0.1.tar.gz", hash = "sha256:4ca091dea149f945ec56afb48dae714f21e8692ef22a395223bcd328961b6a0e"},
 ]
 urllib3 = [
     {file = "urllib3-1.26.7-py2.py3-none-any.whl", hash = "sha256:c4fdf4019605b6e5423637e01bc9fe4daef873709a7973e195ceba0a62bbc844"},
diff --git a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
index 78c6a03b65..eff7216246 100755
--- a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
+++ b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
@@ -88,7 +88,6 @@ def drbg_state(spec, n):
     spec.points_to(llvm.field(state, "v"), v)
     return (state, keyp, cry_f("{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}"))
 
-
 class blob_zero_spec(Contract):
     def __init__(self,n):
         super().__init__()
@@ -97,7 +96,7 @@ def __init__(self,n):
     def specification(self):
         (p, datap) = alloc_blob(self, self.n)
         self.execute_func(p)
-        self.points_to(datap, llvm.cry("zero:[{n}][8]".format(n=self.n)))
+        self.points_to(datap, llvm.cry_f("zero:[{self.n}][8]"))
         self.returns(llvm.cry("0:[32]"))
 
 class increment_drbg_counter_spec(Contract):
@@ -106,7 +105,7 @@ def specification(self):
         v = self.fresh_var(bytes_type(blocksize), "v")
         self.points_to(datap, v)
         self.execute_func(p)
-        self.points_to(datap, llvm.cry("split ((join {v}) +1): [{blocksize}][8]".format(v=v.name(),blocksize=blocksize)))
+        self.points_to(datap, llvm.cry_f("split ((join {v}) +1): [{blocksize}][8]"))
         self.returns(llvm.cry("0:[32]"))
 
 class bytes_used_spec(Contract):
@@ -123,7 +122,7 @@ def specification(self):
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", bytes_type(blocksize))
         outp = alloc_bytes(self, blocksize)
         self.execute_func(keyp, msgp, outp)
-        self.points_to(outp, llvm.cry("encrypt_128 {key} {msg}".format(key=key.name(), msg=msg.name())))
+        self.points_to(outp, llvm.cry_f("encrypt_128 {key} {msg}"))
         self.returns(llvm.cry("0 : [32]"))
 
 class encryptUpdate_spec(Contract):
@@ -135,11 +134,11 @@ def specification(self):
         # but it is constant in the DRBG cryptol specification.
         (key, keyp) = ptr_to_fresh_readonly(self, "key", ctx_type)
         outp = alloc_bytes(self, self.n)
-        lenp = alloc_init(self, llvm_types.i32, llvm.cry("{} : [32]".format(self.n)))
+        lenp = alloc_init(self, llvm_types.i32, llvm.cry_f("{self.n} : [32]"))
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", (bytes_type(self.n)))
-        self.execute_func(keyp, outp, lenp, msgp, llvm.cry("`{blocksize} : [32]".format(blocksize=blocksize)))
-        self.points_to(outp, llvm.cry("encrypt_128 {} {}".format(key.name(), msg.name())))
-        self.points_to(lenp, llvm.cry("{} : [32]".format(self.n)))
+        self.execute_func(keyp, outp, lenp, msgp, llvm.cry_f("`{blocksize} : [32]"))
+        self.points_to(outp, llvm.cry_f("encrypt_128 {key} {msg}"))
+        self.points_to(lenp, llvm.cry_f("{self.n} : [32]"))
         self.returns (llvm.cry("1 : [32]"))
 
 class bits_spec(Contract):
@@ -152,16 +151,16 @@ def specification(self):
         self.execute_func(sp, outp)
         res = cry_f("drbg_generate_internal `{{n={self.n}*8}} {s}")
         # Remove some of the parens here to get really bad error messages
-        c = llvm.cry("split (({res}).0) : [{n}][8]".format(res=res, n=self.n))
+        c = llvm.cry("split (({res}).0) : [{self.n}][8]")
         self.points_to(datap, c)
         ensure_drbg_state(self, sp, keyp, cry_f("{res}.1"))
         self.returns (llvm.cry(" 0 : [32] "))
 
 def ensure_drbg_state(spec, p, keyp, s):
-    spec.points_to(llvm.field(p, "bytes_used"), llvm.cry("({s}).bytes_used".format(s=s)))
+    spec.points_to(llvm.field(p, "bytes_used"), llvm.cry_f("{s}.bytes_used"))
     spec.points_to(llvm.field(p, "ctx"), keyp)
-    spec.points_to(keyp, llvm.cry("split (({s}).ctx.key) : [{keysize}][8]".format(s=s,keysize=keysize)))
-    spec.points_to(llvm.field(p, "v"), llvm.cry("split (({s}).v) : [{blocksize}][8]".format(s=s,blocksize=blocksize)))
+    spec.points_to(keyp, llvm.cry_f("split ({s}.ctx.key) : [{keysize}][8]"))
+    spec.points_to(llvm.field(p, "v"), llvm.cry_f("split ({s}.v) : [{blocksize}][8]"))
     mixes = spec.fresh_var(llvm_types.i64, "mixes")
     spec.points_to(llvm.field(p, "mixes"), mixes)
 
@@ -204,7 +203,7 @@ class cipher_cleanup_spec(Contract):
     def specification(self):
         ctx = self.alloc(ctx_type)
         self.execute_func(ctx)
-        self.points_to(ctx, llvm.cry("zero : [{keysize}][8]".format(keysize=keysize)))
+        self.points_to(ctx, llvm.cry_f("zero : [{keysize}][8]"))
         self.returns(llvm.cry("1:[32]"))
 
 class cipher_key_length_spec(Contract):
@@ -235,7 +234,7 @@ def specification(self):
         (p, datap) = alloc_blob(self, seedsize)
         self.execute_func(p)
         # TODO: blocked on 'fake_entropy'
-        #self.points_to(datap, llvm.cry("split fake_entropy : [{seedsize}][8]".format(seedsize=seedsize)))
+        #self.points_to(datap, llvm.cry_f("split fake_entropy : [{seedsize}][8]"))
         self.returns(llvm.cry("0: [32]"))
 
 class supports_rdrand_spec(Contract):
diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py
index c20e8fb325..b5ffa128af 100644
--- a/saw-remote-api/python/tests/saw/test_salsa20.py
+++ b/saw-remote-api/python/tests/saw/test_salsa20.py
@@ -56,10 +56,10 @@ def specification(self) -> None:
         self.execute_func(y0_p, y1_p, y2_p, y3_p)
 
         res = cry_f("quarterround {[y0, y1, y2, y3]}")
-        self.points_to(y0_p, cry_f("{res} @ 0"))
-        self.points_to(y1_p, cry_f("{res} @ 1"))
-        self.points_to(y2_p, cry_f("{res} @ 2"))
-        self.points_to(y3_p, cry_f("{res} @ 3"))
+        self.points_to(y0_p, cry_f("{res}@0"))
+        self.points_to(y1_p, cry_f("{res}@1"))
+        self.points_to(y2_p, cry_f("{res}@2"))
+        self.points_to(y3_p, cry_f("{res}@3"))
         self.returns(void)
 
 
@@ -102,7 +102,7 @@ def specification(self):
         self.execute_func(k_p, n_p, ks_p)
 
         self.returns(void)
-        self.points_to(ks_p, cry_f("Salsa20_expansion`{{a=2}} {(k, n)}"))
+        self.points_to(ks_p, cry_f("Salsa20_expansion `{{a=2}} {(k, n)}"))
 
 
 

From e77455bc20cda620d07847bfb99f6eefd841d7b3 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 3 Dec 2021 12:49:04 -0800
Subject: [PATCH 3/9] fix types to get mypy passing

---
 saw-remote-api/python/saw_client/__init__.py  |  6 +--
 saw-remote-api/python/saw_client/commands.py  |  4 +-
 .../python/saw_client/connection.py           |  2 +-
 saw-remote-api/python/saw_client/crucible.py  |  4 +-
 .../tests/saw-in-progress/HMAC/spec/HMAC.py   | 29 +++++++------
 .../python/tests/saw-in-progress/drbg/drbg.py | 41 ++++++++++---------
 saw-remote-api/python/tests/saw/test_ghost.py |  4 +-
 7 files changed, 44 insertions(+), 46 deletions(-)

diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py
index 76f2d13dff..fb6bb1e4f8 100644
--- a/saw-remote-api/python/saw_client/__init__.py
+++ b/saw-remote-api/python/saw_client/__init__.py
@@ -624,16 +624,14 @@ def llvm_verify(module: LLVMModule,
 
     return result
 
-def prove(goal: cryptoltypes.CryptolJSON,
-          proof_script: proofscript.ProofScript) -> ProofResult:
+def prove(goal: Any, proof_script: proofscript.ProofScript) -> ProofResult:
     """Atempts to prove that the expression given as the first argument, `goal`, is
     true for all possible values of free symbolic variables. Uses the proof
     script (potentially specifying an automated prover) provided by the second
     argument.
     """
     conn = __get_designated_connection()
-    res = conn.prove(cryptoltypes.to_cryptol(goal),
-                     proof_script.to_json()).result()
+    res = conn.prove(goal, proof_script.to_json()).result()
     pr = ProofResult()
     if res['status'] == 'valid':
         pr.valid = True
diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py
index 257d2b86c5..d61b9c21a5 100644
--- a/saw-remote-api/python/saw_client/commands.py
+++ b/saw-remote-api/python/saw_client/commands.py
@@ -173,10 +173,10 @@ class Prove(SAWCommand):
     def __init__(
             self,
             connection : argo.HasProtocolState,
-            goal : cryptoltypes.CryptolJSON,
+            goal : Any,
             script : ProofScript,
             timeout : Optional[float]) -> None:
-        params = {'goal': goal,
+        params = {'goal': cryptoltypes.to_cryptol(goal) if hasattr(goal, '__to_cryptol__') else goal,
                   'script': script}
         super(Prove, self).__init__('SAW/prove', params, connection, timeout=timeout)
 
diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py
index 8ce464b7a0..b135097843 100644
--- a/saw-remote-api/python/saw_client/connection.py
+++ b/saw-remote-api/python/saw_client/connection.py
@@ -229,7 +229,7 @@ def llvm_assume(self,
         return self.most_recent_result
 
     def prove(self,
-              goal: cryptoltypes.CryptolJSON,
+              goal: Any,
               proof_script: ProofScript,
               timeout : Optional[float] = None) -> Command:
         """Create an instance of the `Prove` command. Documentation on the purpose and
diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index a4ecea079e..3ace58fa22 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -287,7 +287,7 @@ class GhostValue:
     """A class containing the statement that a given ghost variable should have the
     value given by a Cryptol expression.
     """
-    def __init__(self, name: str, value: CryptolTerm) -> None:
+    def __init__(self, name: str, value: cryptoltypes.CryptolJSON) -> None:
         self.name = name
         self.value = value
 
@@ -454,7 +454,7 @@ def points_to(self, pointer : SetupVal, target : SetupVal, *,
         else:
             raise Exception("wrong state")
 
-    def ghost_value(self, var: GhostVariable, value: CryptolTerm) -> None:
+    def ghost_value(self, var: GhostVariable, value: cryptoltypes.CryptolJSON) -> None:
         """Declare that the given ghost variable should have a value specified by the given Cryptol expression.
 
         Usable either before or after `execute_func`.
diff --git a/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py b/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py
index d93049516d..e977e3c556 100644
--- a/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py
+++ b/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py
@@ -1,9 +1,8 @@
 import os
 import os.path
 from cryptol.cryptoltypes import to_cryptol
-from saw import *
-from saw.llvm import Contract, LLVMType, LLVMArrayType, uint8_t, uint32_t, void, SetupVal, FreshVar, cryptol, struct
-import saw.llvm_types as ty
+from saw_client import *
+from saw_client.llvm import *
 from env_server import *
 
 # N.B., transliteration from HMAC.saw
@@ -29,8 +28,8 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, *, re
     
     :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh
              variable will be assigned ``name`` if provided/available.)"""
-    var = c.declare_var(ty, name)
-    ptr = c.alloc(c, ty, points_to=var, read_only=read_only)
+    var = c.fresh_var(ty, name)
+    ptr = c.alloc(ty, points_to=var, read_only=read_only)
     return (var, ptr)
 
 # TODO(AMK) Um... what is this:
@@ -89,16 +88,16 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, *, re
 
 
 def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
-    alg0 = c.fresh_var(ty.i32, "alg")
-    h0 = c.fresh_var(ty.array(8, ty.i64), "h0")
-    Nl0 = c.fresh_var(ty.i64, "Nl")
-    Nh0 = c.fresh_var(ty.i64, "Nh")
-    u0 = c.fresh_var(ty.array(16, ty.i64), "u")
-    num0 = c.fresh_var(ty.i32, "h0")
-    is_ready_for_input0 = c.fresh_var(ty.i8, "is_ready_for_input")
-    currently_in_hash0 = c.fresh_var(ty.i64, "currently_in_hash")
-    md_len0 = c.fresh_var(ty.i32, "md_len")
-    (_, pimpl) = ptr_to_fresh(c, ty.alias('struct.s2n_hash'), "impl", read_only=True)
+    alg0 = c.fresh_var(i32, "alg")
+    h0 = c.fresh_var(array_ty(8, i64), "h0")
+    Nl0 = c.fresh_var(i64, "Nl")
+    Nh0 = c.fresh_var(i64, "Nh")
+    u0 = c.fresh_var(array_ty(16, i64), "u")
+    num0 = c.fresh_var(i32, "h0")
+    is_ready_for_input0 = c.fresh_var(i8, "is_ready_for_input")
+    currently_in_hash0 = c.fresh_var(i64, "currently_in_hash")
+    md_len0 = c.fresh_var(i32, "md_len")
+    (_, pimpl) = ptr_to_fresh(c, alias_ty('struct.s2n_hash'), "impl", read_only=True)
     c.points_to(pstate, 
         struct(
             pimpl,
diff --git a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
index eff7216246..6b0f1232d7 100755
--- a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
+++ b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
@@ -1,15 +1,15 @@
 #!/usr/bin/env python3
 import os
 import os.path
-from saw import *
-from saw.llvm import Contract
-from saw.proofscript import yices
-from cryptol import cry, cryptoltypes
+from saw_client import *
+from saw_client.llvm import Contract, cry, cry_f, array_ty, alias_ty, i8, i32, i64
+from saw_client.proofscript import yices, ProofScript
+from cryptol import cryptoltypes
 #from saw.dashboard import Dashboard
 
 dir_path = os.path.dirname(os.path.realpath(__file__))
-conn = connect("cabal -v0 run exe:saw-remote-api socket")
-view(DebugLog(err=None))
+connect("cabal -v0 run exe:saw-remote-api socket")
+view(DebugLog()) #err=None
 view(LogResults())
 #view(Dashboard(path=__file__))
 
@@ -23,13 +23,13 @@
 mod = llvm_load_module(bcname)
 
 def bytes_type(size):
-    return llvm_types.array(size, llvm_types.i8)
+    return array_ty(size, i8)
 
 blocksize = 16 # blocklen / 8
 keysize = 16 # keylen / 8
 seedsize = 32
 
-blob_type = llvm_types.alias('struct.s2n_blob')
+blob_type = alias_ty('struct.s2n_blob')
 ctx_type = bytes_type(keysize)
 
 def alloc_bytes(spec, n):
@@ -46,7 +46,7 @@ def alloc_blob(spec, n):
 
 def alloc_blob_readonly(spec, n):
     p = spec.alloc(type=blob_type, read_only=True)
-    datap = spec.alloc(llvm_types.array(n, llvm_types.i8), read_only = True)
+    datap = spec.alloc(array_ty(n, i8), read_only = True)
     spec.points_to(llvm.field(p, "data"), datap)
     spec.points_to(llvm.field(p, "size"), llvm.cry_f("`{n}: [32]"))
     return(p, datap)
@@ -77,10 +77,10 @@ def ptr_to_fresh_readonly(spec, n, ty):
     return (x, p)
 
 def drbg_state(spec, n):
-    state = spec.alloc(llvm_types.alias("struct.s2n_drbg"))
+    state = spec.alloc(alias_ty("struct.s2n_drbg"))
     (key, keyp) = ptr_to_fresh(spec, "key", ctx_type)
-    bytes_used = spec.fresh_var(llvm_types.i64, n+"bytes_used")
-    mixes = spec.fresh_var(llvm_types.i64, n+"mixes")
+    bytes_used = spec.fresh_var(i64, n+"bytes_used")
+    mixes = spec.fresh_var(i64, n+"mixes")
     v = spec.fresh_var(bytes_type(blocksize), n+"v")
     spec.points_to(llvm.field(state, "bytes_used"), bytes_used)
     spec.points_to(llvm.field(state, "mixes"), mixes)
@@ -111,7 +111,7 @@ def specification(self):
 class bytes_used_spec(Contract):
     def specification(self):
         (sp, keyp, s) = drbg_state(self,"drbg")
-        bytes_used = alloc_init(self, llvm_types.i64, llvm.cry("0:[64]"))
+        bytes_used = alloc_init(self, i64, llvm.cry("0:[64]"))
         self.execute_func(sp, bytes_used)
         self.points_to(bytes_used, llvm.cry_f("{s}.bytes_used"))
         self.returns(llvm.cry("0:[32]"))
@@ -134,7 +134,7 @@ def specification(self):
         # but it is constant in the DRBG cryptol specification.
         (key, keyp) = ptr_to_fresh_readonly(self, "key", ctx_type)
         outp = alloc_bytes(self, self.n)
-        lenp = alloc_init(self, llvm_types.i32, llvm.cry_f("{self.n} : [32]"))
+        lenp = alloc_init(self, i32, llvm.cry_f("{self.n} : [32]"))
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", (bytes_type(self.n)))
         self.execute_func(keyp, outp, lenp, msgp, llvm.cry_f("`{blocksize} : [32]"))
         self.points_to(outp, llvm.cry_f("encrypt_128 {key} {msg}"))
@@ -161,7 +161,7 @@ def ensure_drbg_state(spec, p, keyp, s):
     spec.points_to(llvm.field(p, "ctx"), keyp)
     spec.points_to(keyp, llvm.cry_f("split ({s}.ctx.key) : [{keysize}][8]"))
     spec.points_to(llvm.field(p, "v"), llvm.cry_f("split ({s}.v) : [{blocksize}][8]"))
-    mixes = spec.fresh_var(llvm_types.i64, "mixes")
+    mixes = spec.fresh_var(i64, "mixes")
     spec.points_to(llvm.field(p, "mixes"), mixes)
 
 #////////////////////////////////////////////////////////////////////////////////
@@ -170,7 +170,7 @@ def ensure_drbg_state(spec, p, keyp, s):
 
 class getenv_spec(Contract):
     def specification(self):
-        p = self.alloc(llvm_types.i8)
+        p = self.alloc(i8)
         self.execute_func(p)
         self.returns(llvm.null)
 
@@ -240,7 +240,7 @@ def specification(self):
 class supports_rdrand_spec(Contract):
     def specification(self):
         self.execute_func()
-        r = self.fresh_var(llvm_types.i8, "supports_rdrand")
+        r = self.fresh_var(i8, "supports_rdrand")
         self.returns(r)
 
 #////////////////////////////////////////////////////////////////////////////////
@@ -299,14 +299,15 @@ def specification(self):
 llvm_verify(mod, "s2n_drbg_bytes_used", bytes_used_spec())
 
 
-blk_enc_ov = llvm_verify(mod, "s2n_drbg_block_encrypt", contract = block_encrypt_spec(), lemmas = [encryptUpdate_ov], script = yices(unints=['block_encrypt']))
+blk_enc_ov = llvm_verify(mod, "s2n_drbg_block_encrypt", contract = block_encrypt_spec(),
+        lemmas = [encryptUpdate_ov], script = ProofScript([yices(unints=['block_encrypt'])]))
 
 bits_ov = llvm_verify(mod, "s2n_drbg_bits", contract = bits_spec(seedsize),
-        lemmas = [inc_ov, encryptUpdate_ov, blk_enc_ov], script = yices(['block_encrypt']))
+        lemmas = [inc_ov, encryptUpdate_ov, blk_enc_ov], script = ProofScript([yices(['block_encrypt'])]))
 
 update_ov = llvm_verify(mod, "s2n_drbg_update", lemmas = [bits_ov,
     encryptInit_ov, aes_128_ecb_ov, cipher_key_length_ov], contract=
-    update_spec(seedsize), script = yices(["block_encrypt"]))
+    update_spec(seedsize), script = ProofScript([yices(["block_encrypt"])]))
 
 # TODO: this lemma cannot be proven yet, see drbg-helpers.cry for the definition
 # of "fake_entropy"
diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py
index 5bddda8fd5..265934f080 100644
--- a/saw-remote-api/python/tests/saw/test_ghost.py
+++ b/saw-remote-api/python/tests/saw/test_ghost.py
@@ -14,7 +14,7 @@ def post_counter(contract: Contract, counter: GhostVariable, n: CryptolTerm):
     contract.ghost_value(counter, cry_f("{n} + 1"))
 
 class GetAndIncrementContract(Contract):
-    def __init__(self, counter: str) -> None:
+    def __init__(self, counter: GhostVariable) -> None:
         super().__init__()
         self.counter = counter
 
@@ -25,7 +25,7 @@ def specification(self) -> None:
         self.returns(n)
 
 class FContract(Contract):
-    def __init__(self, counter: str) -> None:
+    def __init__(self, counter: GhostVariable) -> None:
         super().__init__()
         self.counter = counter
 

From ac81c6d0f409d4d718ae066e0a4622d2590069c5 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 23 Dec 2021 13:47:17 -0800
Subject: [PATCH 4/9] update to cryptol_client 2.12.2, add JSON type

---
 deps/cryptol                                  |  2 +-
 saw-remote-api/python/poetry.lock             | 48 +++++++------
 saw-remote-api/python/pyproject.toml          |  4 +-
 saw-remote-api/python/saw_client/crucible.py  | 68 ++++++++-----------
 saw-remote-api/python/tests/saw/test_ghost.py |  4 +-
 .../python/tests/saw/test_salsa20.py          |  4 +-
 6 files changed, 59 insertions(+), 71 deletions(-)

diff --git a/deps/cryptol b/deps/cryptol
index abb41f5b4e..34404d7930 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit abb41f5b4e16bfc351ec6c6a6a419c36fd94ac10
+Subproject commit 34404d7930d82b8b96c5ccc32d8ae5a7ba033e5e
diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock
index c4e4413bf6..c10a5a223e 100644
--- a/saw-remote-api/python/poetry.lock
+++ b/saw-remote-api/python/poetry.lock
@@ -1,14 +1,14 @@
 [[package]]
 name = "argo-client"
-version = "0.0.9"
+version = "0.0.10"
 description = "A JSON RPC client library."
 category = "main"
 optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.7.0,<4"
 
 [package.dependencies]
-mypy = "*"
-requests = "*"
+requests = ">=2.26.0,<3.0.0"
+urllib3 = ">=1.26.5"
 
 [[package]]
 name = "bitvector"
@@ -28,7 +28,7 @@ python-versions = "*"
 
 [[package]]
 name = "charset-normalizer"
-version = "2.0.8"
+version = "2.0.9"
 description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet."
 category = "main"
 optional = false
@@ -39,21 +39,16 @@ unicode_backport = ["unicodedata2"]
 
 [[package]]
 name = "cryptol"
-version = "2.12.1"
+version = "2.12.2"
 description = "Cryptol client for the Cryptol 2.12 RPC server"
 category = "main"
 optional = false
-python-versions = ">=3.7.0"
-develop = true
+python-versions = ">=3.7.0,<4"
 
 [package.dependencies]
-argo-client = "0.0.9"
-BitVector = "^3.4.9"
-requests = "^2.25.1"
-
-[package.source]
-type = "directory"
-url = "../../deps/cryptol/cryptol-remote-api/python"
+argo-client = "0.0.10"
+BitVector = ">=3.4.9,<4.0.0"
+requests = ">=2.25.1,<3.0.0"
 
 [[package]]
 name = "idna"
@@ -67,7 +62,7 @@ python-versions = ">=3.5"
 name = "mypy"
 version = "0.812"
 description = "Optional static typing for Python"
-category = "main"
+category = "dev"
 optional = false
 python-versions = ">=3.5"
 
@@ -83,7 +78,7 @@ dmypy = ["psutil (>=4.0)"]
 name = "mypy-extensions"
 version = "0.4.3"
 description = "Experimental type system extensions for programs checked with the mypy typechecker."
-category = "main"
+category = "dev"
 optional = false
 python-versions = "*"
 
@@ -109,7 +104,7 @@ use_chardet_on_py3 = ["chardet (>=3.0.2,<5)"]
 name = "typed-ast"
 version = "1.4.3"
 description = "a fork of Python 2 and 3 ast modules with type comment support"
-category = "main"
+category = "dev"
 optional = false
 python-versions = "*"
 
@@ -117,7 +112,7 @@ python-versions = "*"
 name = "typing-extensions"
 version = "4.0.1"
 description = "Backported and Experimental Type Hints for Python 3.6+"
-category = "main"
+category = "dev"
 optional = false
 python-versions = ">=3.6"
 
@@ -137,12 +132,12 @@ socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"]
 [metadata]
 lock-version = "1.1"
 python-versions = "^3.8"
-content-hash = "d1ec6c507e7a1f0f935f625feec468b2291974cc537e2891f1f0bbfcc70416bb"
+content-hash = "ffca6578b36152988e9e38f2f828a6807ae038cf3ff2722610a03af90f4b7586"
 
 [metadata.files]
 argo-client = [
-    {file = "argo-client-0.0.9.tar.gz", hash = "sha256:762e16d7428046ecf1d4fd50d877cba9a3c21eac260806030876f76acac81325"},
-    {file = "argo_client-0.0.9-py3-none-any.whl", hash = "sha256:c482e3ba3346c7677fc1c8a470b173ba0d59736d6c628b0193a13b8e3aeeb9f1"},
+    {file = "argo-client-0.0.10.tar.gz", hash = "sha256:a95e07201a5e23758e7bc6b2e1d594c61a71df02ff534ad7a8db32fdb991ed0b"},
+    {file = "argo_client-0.0.10-py3-none-any.whl", hash = "sha256:d86e07bfc421faf9f25be6af2d4a0c7fd2ddef7a759488f6c05baa2ff2c1e390"},
 ]
 bitvector = [
     {file = "BitVector-3.5.0.tar.gz", hash = "sha256:cac2fbccf11e325115827ed7be03e5fd62615227b0bbf3fa5a18a842a221839c"},
@@ -152,10 +147,13 @@ certifi = [
     {file = "certifi-2021.10.8.tar.gz", hash = "sha256:78884e7c1d4b00ce3cea67b44566851c4343c120abd683433ce934a68ea58872"},
 ]
 charset-normalizer = [
-    {file = "charset-normalizer-2.0.8.tar.gz", hash = "sha256:735e240d9a8506778cd7a453d97e817e536bb1fc29f4f6961ce297b9c7a917b0"},
-    {file = "charset_normalizer-2.0.8-py3-none-any.whl", hash = "sha256:83fcdeb225499d6344c8f7f34684c2981270beacc32ede2e669e94f7fa544405"},
+    {file = "charset-normalizer-2.0.9.tar.gz", hash = "sha256:b0b883e8e874edfdece9c28f314e3dd5badf067342e42fb162203335ae61aa2c"},
+    {file = "charset_normalizer-2.0.9-py3-none-any.whl", hash = "sha256:1eecaa09422db5be9e29d7fc65664e6c33bd06f9ced7838578ba40d58bdf3721"},
+]
+cryptol = [
+    {file = "cryptol-2.12.2-py3-none-any.whl", hash = "sha256:d543f2a92b0000f869576c89eeee2fa19ddeb064193a13ce8e55f1e6a388a60b"},
+    {file = "cryptol-2.12.2.tar.gz", hash = "sha256:ca2d84557354387b8f856902e18333fb1b6792cbf0e10173e1b64854af085ec7"},
 ]
-cryptol = []
 idna = [
     {file = "idna-3.3-py3-none-any.whl", hash = "sha256:84d9dd047ffa80596e0f246e2eab0b391788b0503584e8945f2368256d2735ff"},
     {file = "idna-3.3.tar.gz", hash = "sha256:9d643ff0a55b762d5cdb124b8eaa99c66322e2157b69160bc32796e824360e6d"},
diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml
index 86f8ce85ae..c0793d0e35 100644
--- a/saw-remote-api/python/pyproject.toml
+++ b/saw-remote-api/python/pyproject.toml
@@ -14,8 +14,8 @@ include = [
 python = "^3.8"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
-argo-client = "~0.0.6"
+cryptol = "2.12.2" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
+argo-client = "0.0.10"
 
 [tool.poetry.dev-dependencies]
 mypy = "^0.812"
diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index 3ace58fa22..bb855e032b 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -5,7 +5,7 @@
 from dataclasses import dataclass
 import dataclasses
 import re
-from typing import Any, Dict, List, Optional, Set, Union, overload
+from typing import Any, Dict, List, Tuple, Optional, Set, Union, overload
 from typing_extensions import Literal
 import inspect
 import uuid
@@ -13,6 +13,8 @@
 from .llvm_type import *
 from .jvm_type import *
 
+JSON = Union[None, bool, int, float, str, Dict, Tuple, List]
+
 class SetupVal(metaclass=ABCMeta):
     """Represent a ``SetupValue`` in SawScript, which "corresponds to
     values that can occur during symbolic execution, which includes both 'Term'
@@ -20,7 +22,7 @@ class SetupVal(metaclass=ABCMeta):
     (both structures and arrays)."
     """
     @abstractmethod
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         """JSON representation for this ``SetupVal`` (i.e., how it is represented in expressions, etc).
 
         N.B., should be a JSON object with a ``'setup value'`` field with a unique tag which the
@@ -51,7 +53,7 @@ class NamedSetupVal(SetupVal):
     """Represents those ``SetupVal``s which are a named reference to some value, e.e., a variable
     or reference to allocated memory."""
     @abstractmethod
-    def to_init_json(self) -> Any:
+    def to_init_json(self) -> JSON:
         """JSON representation with the information for those ``SetupVal``s which require additional
         information to initialize/allocate them vs that which is required later to reference them.
 
@@ -70,20 +72,16 @@ def __init__(self, code : Union[str, cryptoltypes.CryptolJSON]):
             self.expression = code
 
     def __call__(self, *args : cryptoltypes.CryptolJSON) -> 'CryptolTerm':
-        out_term = self.expression
-        for a in args:
-            out_term = cryptoltypes.CryptolApplication(out_term, a)
-
-        return CryptolTerm(out_term)
+        return CryptolTerm(cryptoltypes.CryptolApplication(self.expression, *args))
 
     def __repr__(self) -> str:
         return f"CryptolTerm({self.expression!r})"
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'Cryptol', 'expression': cryptoltypes.to_cryptol(self.expression)}
 
-    def __to_cryptol__(self, ty : Any) -> cryptoltypes.JSON:
-        return self.expression.__to_cryptol__(ty)
+    def __to_cryptol__(self) -> cryptoltypes.JSON:
+        return self.expression.__to_cryptol__()
 
     def __to_cryptol_str__(self) -> str:
         return self.expression.__to_cryptol_str__()
@@ -96,13 +94,13 @@ def __init__(self, spec : 'Contract', type : Union['LLVMType', 'JVMType'], sugge
         self.spec = spec
         self.type = type
 
-    def __to_cryptol__(self, ty : Any) -> cryptoltypes.JSON:
-        return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__(ty)
+    def __to_cryptol__(self) -> cryptoltypes.JSON:
+        return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__()
 
     def __to_cryptol_str__(self) -> str:
         return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol_str__()
 
-    def to_init_json(self) -> Any:
+    def to_init_json(self) -> JSON:
         #FIXME it seems we don't actually use two names ever... just the one...do we actually need both?
         name = self.name()
         return {"server name": name,
@@ -114,17 +112,9 @@ def name(self) -> str:
             self.__name = self.spec.get_fresh_name()
         return self.__name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'named', 'name': self.name()}
 
-    def __gt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm:
-        gt = CryptolTerm("(>)")
-        return gt(self, other)
-
-    def __lt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm:
-        lt = CryptolTerm("(<)")
-        return lt(self, other)
-
 
 class Allocated(NamedSetupVal):
     name : Optional[str]
@@ -137,7 +127,7 @@ def __init__(self, spec : 'Contract', type : Union['LLVMType','JVMType'], *,
         self.mutable = mutable
         self.alignment = alignment
 
-    def to_init_json(self) -> Any:
+    def to_init_json(self) -> JSON:
         if self.name is None:
             self.name = self.spec.get_fresh_name()
         return {"server name": self.name,
@@ -145,7 +135,7 @@ def to_init_json(self) -> Any:
                 "mutable": self.mutable,
                 "alignment": self.alignment}
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         if self.name is None:
             self.name = self.spec.get_fresh_name()
         return {'setup value': 'named', 'name': self.name}
@@ -156,7 +146,7 @@ class StructVal(SetupVal):
     def __init__(self, fields : List[SetupVal]) -> None:
         self.fields = fields
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'tuple', 'elements': [fld.to_json() for fld in self.fields]}
 
 class ElemVal(SetupVal):
@@ -167,7 +157,7 @@ def __init__(self, base : SetupVal, index : int) -> None:
         self.base = base
         self.index = index
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'element lvalue',
                 'base': self.base.to_json(), 'index': self.index}
 
@@ -179,7 +169,7 @@ def __init__(self, base : SetupVal, field_name : str) -> None:
         self.base = base
         self.field_name = field_name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'field',
                 'base': self.base.to_json(), 'field': self.field_name}
 
@@ -189,7 +179,7 @@ class GlobalInitializerVal(SetupVal):
     def __init__(self, name : str) -> None:
         self.name = name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'global initializer', 'name': self.name}
 
 class GlobalVarVal(SetupVal):
@@ -198,11 +188,11 @@ class GlobalVarVal(SetupVal):
     def __init__(self, name : str) -> None:
         self.name = name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'global lvalue', 'name': self.name}
 
 class NullVal(SetupVal):
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'null'}
 
 class ArrayVal(SetupVal):
@@ -211,7 +201,7 @@ class ArrayVal(SetupVal):
     def __init__(self, elements : List[SetupVal]) -> None:
         self.elements = elements
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'array',
                 'elements': [element.to_json() for element in self.elements]}
 
@@ -249,7 +239,7 @@ class Condition:
     def __init__(self, condition : CryptolTerm) -> None:
         self.cryptol_term = condition
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return cryptoltypes.to_cryptol(self.cryptol_term)
 
 
@@ -264,7 +254,7 @@ def __init__(self, pointer : SetupVal, target : SetupVal, *,
         self.check_target_type = check_target_type
         self.condition = condition
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         check_target_type_json: Optional[Dict[str, Any]]
         if self.check_target_type is None:
             check_target_type_json = None
@@ -291,7 +281,7 @@ def __init__(self, name: str, value: cryptoltypes.CryptolJSON) -> None:
         self.name = name
         self.value = value
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {"server name": self.name,
                 "value": cryptoltypes.to_cryptol(self.value)}
 
@@ -304,7 +294,7 @@ class State:
     points_to : List[PointsTo] = dataclasses.field(default_factory=list)
     ghost_values : List[GhostValue] = dataclasses.field(default_factory=list)
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'variables': [v.to_init_json() for v in self.fresh],
                 'conditions': [c.to_json() for c in self.conditions],
                 'allocated': [a.to_init_json() for a in self.allocated],
@@ -319,7 +309,7 @@ def to_json(self) -> Any:
 
 @dataclass
 class Void:
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return None
 
 void = Void()
@@ -351,7 +341,7 @@ class Contract:
     __definition_lineno : Optional[int]
     __definition_filename : Optional[str]
     __unique_id : uuid.UUID
-    __cached_json : Optional[Any]
+    __cached_json : JSON
 
     def __init__(self) -> None:
         self.__pre_state = State(self)
@@ -535,7 +525,7 @@ def definition_lineno(self) -> Optional[int]:
     def definition_filename(self) -> Optional[str]:
         return self.__definition_filename
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         if self.__cached_json is not None:
             return self.__cached_json
         else:
diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py
index 265934f080..f916f45330 100644
--- a/saw-remote-api/python/tests/saw/test_ghost.py
+++ b/saw-remote-api/python/tests/saw/test_ghost.py
@@ -6,7 +6,7 @@
 
 def pre_counter(contract: Contract, counter: GhostVariable):
     n = contract.fresh_var(i32, "n")
-    contract.precondition(n < cry("128"))
+    contract.precondition(cry_f("{n} < 128"))
     contract.ghost_value(counter, n)
     return n
 
@@ -32,7 +32,7 @@ def __init__(self, counter: GhostVariable) -> None:
     def specification(self) -> None:
         n = pre_counter(self, self.counter)
         i = self.fresh_var(i32, "i")
-        self.precondition(i < cry("512"))
+        self.precondition(cry_f("{i} < 512"))
         self.execute_func(i)
         post_counter(self, self.counter, n)
         self.returns(cry_f("{i} * {n}"))
diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py
index b5ffa128af..e514e8aac1 100644
--- a/saw-remote-api/python/tests/saw/test_salsa20.py
+++ b/saw-remote-api/python/tests/saw/test_salsa20.py
@@ -32,8 +32,8 @@ class RotlContract(Contract):
     def specification(self) -> None:
         value = self.fresh_var(i32, "value")
         shift = self.fresh_var(i32, "shift")
-        self.precondition(shift > cry("0"))
-        self.precondition(shift < cry("32"))
+        self.precondition(cry_f("{shift} > 0"))
+        self.precondition(cry_f("{shift} < 32"))
 
         self.execute_func(value, shift)
 

From ab2d646b2cf8a8430079d43cfae35c48373fc8f8 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 23 Dec 2021 14:23:41 -0800
Subject: [PATCH 5/9] add precondition_f, postcondition_f, returns_f, update
 tests

---
 saw-remote-api/python/saw_client/crucible.py  | 21 +++++++++++++++++++
 .../python/tests/saw/test_basic_java.py       |  4 ++--
 saw-remote-api/python/tests/saw/test_ghost.py |  6 +++---
 .../saw/test_llvm_lax_pointer_ordering.py     |  4 ++--
 .../tests/saw/test_llvm_points_to_bitfield.py |  8 +++----
 .../python/tests/saw/test_llvm_struct.py      |  2 +-
 .../python/tests/saw/test_salsa20.py          |  6 +++---
 7 files changed, 36 insertions(+), 15 deletions(-)

diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index 28cc6f16df..79077c3901 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -521,6 +521,13 @@ def precondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.Crypto
         else:
             raise Exception("preconditions must be specified before execute_func is called in the contract")
 
+    def precondition_f(self, s : str) -> None:
+        """Parses the given string like ``cry_f``, then calls ``precondition``
+        on the result.
+        """
+        expression = to_cryptol_str_customf(s, frames=1, filename="<precondition_f>")
+        return self.precondition(expression)
+
     def postcondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None:
         """Establishes ``proposition`` as a postcondition for the function ```Contract```
         being specified.
@@ -535,6 +542,13 @@ def postcondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.Crypt
         else:
             raise Exception("postconditions must be specified after execute_func is called in the contract")
 
+    def postcondition_f(self, s : str) -> None:
+        """Parses the given string like ``cry_f``, then calls ``postcondition``
+        on the result.
+        """
+        expression = to_cryptol_str_customf(s, frames=1, filename="<postcondition_f>")
+        return self.postcondition(expression)
+
     def returns(self, val : Union[Void,SetupVal]) -> None:
         if self.__state == 'post':
             if self.__returns is None:
@@ -544,6 +558,13 @@ def returns(self, val : Union[Void,SetupVal]) -> None:
         else:
             raise ValueError("Not in postcondition")
 
+    def returns_f(self, s : str) -> None:
+        """Parses the given string like ``cry_f``, then calls ``returns``
+        on the result.
+        """
+        expression = to_cryptol_str_customf(s, frames=1, filename="<returns_f>")
+        return self.returns(CryptolTerm(expression))
+
     def lemma_name(self, hint  : Optional[str] = None) -> str:
         if hint is None:
             hint = self.__class__.__name__
diff --git a/saw-remote-api/python/tests/saw/test_basic_java.py b/saw-remote-api/python/tests/saw/test_basic_java.py
index 0267006889..43ba2bda26 100644
--- a/saw-remote-api/python/tests/saw/test_basic_java.py
+++ b/saw-remote-api/python/tests/saw/test_basic_java.py
@@ -15,7 +15,7 @@ def specification(self) -> None:
 
         self.execute_func(x, y)
 
-        self.returns(cry_f("{x} + {y}"))
+        self.returns_f("{x} + {y}")
 
 class Double(Contract):
     def __init__(self) -> None:
@@ -26,7 +26,7 @@ def specification(self) -> None:
 
         self.execute_func(x)
 
-        self.returns(cry_f("{x} + {x}"))
+        self.returns_f("{x} + {x}")
 
 class AddTest(unittest.TestCase):
     def test_add(self):
diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py
index f916f45330..a9a05e4a6b 100644
--- a/saw-remote-api/python/tests/saw/test_ghost.py
+++ b/saw-remote-api/python/tests/saw/test_ghost.py
@@ -6,7 +6,7 @@
 
 def pre_counter(contract: Contract, counter: GhostVariable):
     n = contract.fresh_var(i32, "n")
-    contract.precondition(cry_f("{n} < 128"))
+    contract.precondition_f("{n} < 128")
     contract.ghost_value(counter, n)
     return n
 
@@ -32,10 +32,10 @@ def __init__(self, counter: GhostVariable) -> None:
     def specification(self) -> None:
         n = pre_counter(self, self.counter)
         i = self.fresh_var(i32, "i")
-        self.precondition(cry_f("{i} < 512"))
+        self.precondition_f("{i} < 512")
         self.execute_func(i)
         post_counter(self, self.counter, n)
-        self.returns(cry_f("{i} * {n}"))
+        self.returns_f("{i} * {n}")
 
 class GhostTest(unittest.TestCase):
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py b/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
index cea240f5dd..8cb94fa36e 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
@@ -1,7 +1,7 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, FreshVar, LLVMType, SetupVal, array_ty, cryptol, i64, void
+from saw_client.llvm import Contract, FreshVar, LLVMType, SetupVal, array_ty, cry, cry_f, i64, void
 from saw_client.option import LaxPointerOrdering
 
 
@@ -29,7 +29,7 @@ def specification(self):
 
         self.execute_func(c_ptr, a_ptr, b_ptr)
 
-        self.points_to(c_ptr, cryptol(f'zipWith`{{ {LEN} }} (+) {a.name()} {b.name()}'))
+        self.points_to(c_ptr, cry_f('zipWith`{{ {LEN} }} (+) {a} {b}'))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
index 10f3f5e6d7..96d6dfcec9 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
@@ -1,7 +1,7 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, LLVMIntType, alias_ty, cryptol, i8, void
+from saw_client.llvm import Contract, LLVMIntType, alias_ty, cry, cry_f, i8, void
 from saw_client.option import LaxLoadsAndStores
 
 
@@ -17,7 +17,7 @@ def specification(self):
 
         self.execute_func(ss)
 
-        self.returns(cryptol(f'zext {z.name()} : [8]'))
+        self.returns_f('zext {z} : [8]')
 
 
 class GetYContract(Contract):
@@ -38,7 +38,7 @@ def specification(self):
 
         self.execute_func(ss, z)
 
-        self.points_to_bitfield(ss, 'x2', cryptol(f'drop {z.name()} : [2]'))
+        self.points_to_bitfield(ss, 'x2', cry_f('drop {z} : [2]'))
         self.returns(void)
 
 
@@ -47,7 +47,7 @@ def specification(self):
         ss = self.alloc(alias_ty('struct.s'))
         z = self.fresh_var(i2, 'z')
 
-        self.execute_func(ss, cryptol(f'zext {z.name()} : [8]'))
+        self.execute_func(ss, cry_f('zext {z} : [8]'))
 
         self.points_to_bitfield(ss, 'x2', z)
         self.returns(void)
diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct.py b/saw-remote-api/python/tests/saw/test_llvm_struct.py
index 03408bf8a1..8702782de5 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_struct.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_struct.py
@@ -33,7 +33,7 @@ def specification(self):
 
         self.execute_func(p)
 
-        self.returns(cry_f('{x}@0 + {x}@1'))
+        self.returns_f('{x}@0 + {x}@1')
 
 
 class IdContract(Contract):
diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py
index e514e8aac1..f2d13f96e7 100644
--- a/saw-remote-api/python/tests/saw/test_salsa20.py
+++ b/saw-remote-api/python/tests/saw/test_salsa20.py
@@ -32,12 +32,12 @@ class RotlContract(Contract):
     def specification(self) -> None:
         value = self.fresh_var(i32, "value")
         shift = self.fresh_var(i32, "shift")
-        self.precondition(cry_f("{shift} > 0"))
-        self.precondition(cry_f("{shift} < 32"))
+        self.precondition_f("{shift} > 0")
+        self.precondition_f("{shift} < 32")
 
         self.execute_func(value, shift)
 
-        self.returns(cry_f("{value} <<< {shift}"))
+        self.returns_f("{value} <<< {shift}")
 
 
 

From bacdc5871fbc1ef60e91b1dc8e050f63e191f0a7 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 23 Dec 2021 14:28:39 -0800
Subject: [PATCH 6/9] fix type of `prove` for mypy

---
 saw-remote-api/python/saw_client/__init__.py   | 3 ++-
 saw-remote-api/python/saw_client/commands.py   | 4 ++--
 saw-remote-api/python/saw_client/connection.py | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py
index 1a6292c627..4a2a412368 100644
--- a/saw-remote-api/python/saw_client/__init__.py
+++ b/saw-remote-api/python/saw_client/__init__.py
@@ -625,7 +625,8 @@ def llvm_verify(module: LLVMModule,
 
     return result
 
-def prove(goal: Any, proof_script: proofscript.ProofScript) -> ProofResult:
+def prove(goal: cryptoltypes.CryptolJSON,
+          proof_script: proofscript.ProofScript) -> ProofResult:
     """Atempts to prove that the expression given as the first argument, `goal`, is
     true for all possible values of free symbolic variables. Uses the proof
     script (potentially specifying an automated prover) provided by the second
diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py
index a2d6fc0895..d6d0263cac 100644
--- a/saw-remote-api/python/saw_client/commands.py
+++ b/saw-remote-api/python/saw_client/commands.py
@@ -174,10 +174,10 @@ class Prove(SAWCommand):
     def __init__(
             self,
             connection : argo.HasProtocolState,
-            goal : Any,
+            goal : cryptoltypes.CryptolJSON,
             script : ProofScript,
             timeout : Optional[float]) -> None:
-        params = {'goal': cryptoltypes.to_cryptol(goal) if hasattr(goal, '__to_cryptol__') else goal,
+        params = {'goal': cryptoltypes.to_cryptol(goal),
                   'script': script}
         super(Prove, self).__init__('SAW/prove', params, connection, timeout=timeout)
 
diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py
index 95c398d871..0004f09db4 100644
--- a/saw-remote-api/python/saw_client/connection.py
+++ b/saw-remote-api/python/saw_client/connection.py
@@ -230,7 +230,7 @@ def llvm_assume(self,
         return self.most_recent_result
 
     def prove(self,
-              goal: Any,
+              goal: cryptoltypes.CryptolJSON,
               proof_script: ProofScript,
               timeout : Optional[float] = None) -> Command:
         """Create an instance of the `Prove` command. Documentation on the purpose and

From aedd4cef980593fb01b4bd947f7a2ee7c2b2504d Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 24 Dec 2021 11:58:25 -0800
Subject: [PATCH 7/9] improve comments, revert some types, import cry_f from
 crucible in tests

---
 saw-remote-api/python/saw_client/crucible.py  | 73 +++++++++++++------
 .../python/tests/saw-in-progress/drbg/drbg.py | 63 ++++++++--------
 .../python/tests/saw/test_alloc_aligned.py    |  3 +-
 .../python/tests/saw/test_basic_java.py       |  3 +-
 saw-remote-api/python/tests/saw/test_ghost.py |  3 +-
 .../python/tests/saw/test_llvm_assert_null.py |  3 +-
 .../saw/test_llvm_lax_pointer_ordering.py     |  3 +-
 .../python/tests/saw/test_llvm_pointer.py     |  3 +-
 .../tests/saw/test_llvm_points_to_bitfield.py |  3 +-
 .../python/tests/saw/test_llvm_struct.py      |  3 +-
 .../python/tests/saw/test_llvm_struct_type.py |  3 +-
 .../tests/saw/test_points_to_at_type.py       |  3 +-
 .../python/tests/saw/test_salsa20.py          |  3 +-
 13 files changed, 106 insertions(+), 63 deletions(-)

diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index 79077c3901..16c5d7a385 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -522,9 +522,8 @@ def precondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.Crypto
             raise Exception("preconditions must be specified before execute_func is called in the contract")
 
     def precondition_f(self, s : str) -> None:
-        """Parses the given string like ``cry_f``, then calls ``precondition``
-        on the result.
-        """
+        """Declares a precondition using a ``cry_f``-style format string, i.e.
+        ``precondition_f(...)`` is equivalent to ``precondition(cry_f(...))``"""
         expression = to_cryptol_str_customf(s, frames=1, filename="<precondition_f>")
         return self.precondition(expression)
 
@@ -543,9 +542,8 @@ def postcondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.Crypt
             raise Exception("postconditions must be specified after execute_func is called in the contract")
 
     def postcondition_f(self, s : str) -> None:
-        """Parses the given string like ``cry_f``, then calls ``postcondition``
-        on the result.
-        """
+        """Declares a postcondition using a ``cry_f``-style format string, i.e.
+        ``postcondition_f(...)`` is equivalent to ``postcondition(cry_f(...))``"""
         expression = to_cryptol_str_customf(s, frames=1, filename="<postcondition_f>")
         return self.postcondition(expression)
 
@@ -559,9 +557,8 @@ def returns(self, val : Union[Void,SetupVal]) -> None:
             raise ValueError("Not in postcondition")
 
     def returns_f(self, s : str) -> None:
-        """Parses the given string like ``cry_f``, then calls ``returns``
-        on the result.
-        """
+        """Declares a return value using a ``cry_f``-style format string, i.e.
+        ``returns_f(...)`` is equivalent to ``returns(cry_f(...))``"""
         expression = to_cryptol_str_customf(s, frames=1, filename="<returns_f>")
         return self.returns(CryptolTerm(expression))
 
@@ -622,21 +619,55 @@ def to_json(self) -> JSON:
 
 # It's tempting to name this `global` to mirror SAWScript's `llvm_global`,
 # but that would clash with the Python keyword `global`.
-def global_var(name: str) -> GlobalVarVal:
+def global_var(name: str) -> SetupVal:
     """Returns a pointer to the named global ``name`` (i.e., a ``GlobalVarVal``)."""
     return GlobalVarVal(name)
 
 def cry(s : str) -> CryptolTerm:
-    """Like ``cry`` from the Cryptol bindings, but retuns a ``CryptolTerm``
-    (which is also a ``SetupVal``)."""
+    """Embed a string of Cryptol syntax as a ``CryptolTerm`` (which is also a
+       ``SetupVal``) - also see ``cry_f``."""
     return CryptolTerm(s)
 
 def cry_f(s : str) -> CryptolTerm:
-    """Like ``cry_f`` from the Cryptol bindings, but retuns a ``CryptolTerm``
-    (which is also a ``SetupVal``)."""
-    return CryptolTerm(to_cryptol_str_customf(s, frames=1, filename='<cryptol_f>'))
+    """Embed a string of Cryptol syntax as a ``CryptolTerm`` (which is also a
+       ``SetupVal``), where the given string is parsed as an f-string, and the
+       values within brackets are converted to Cryptol syntax using
+       ``to_cryptol_str`` from the Cryptol Python library.
+
+       Like f-strings, values in brackets (``{``, ``}``) are parsed as python
+       expressions in the caller's context of local and global variables, and
+       to include a literal bracket in the final string, it must be doubled
+       (i.e. ``{{`` or ``}}``). The latter is needed when using explicit type
+       application or record syntax. For example, if ``x = [0,1]`` then
+       ``cry_f('length `{{2}} {x}')`` is equal to ``cry('length `{2} [0,1]')``
+       and ``cry_f('{{ x = {x} }}')`` is equal to ``cry('{ x = [0,1] }')``.
+
+       When formatting Cryptol, it is recomended to use this function rather
+       than any of python's built-in methods of string formatting (e.g.
+       f-strings, ``str.format``) as the latter will not always produce valid
+       Cryptol syntax. Specifically, this function differs from these methods
+       in the cases of ``BV``s, string literals, function application (this
+       function will add parentheses as needed), and dicts. For example,
+       ``cry_f('{ {"x": 5, "y": 4} }')`` equals ``cry('{x = 5, y = 4}')``
+       but ``f'{ {"x": 5, "y": 4} }'`` equals ``'{"x": 5, "y": 4}'``. Only
+       the former is valid Cryptol syntax for a record.
+       
+       Note that any conversion or format specifier will always result in the
+       argument being rendered as a Cryptol string literal with the conversion
+       and/or formating applied. For example, `cry('f {5}')` is equal to
+       ``cry('f 5')`` but ``cry_f('f {5!s}')`` is equal to ``cry(`f "5"`)``
+       and ``cry_f('f {5:+.2%}')`` is equal to ``cry('f "+500.00%"')``.
+
+       :example:
+
+       >>> x = BV(size=7, value=1)
+       >>> y = cry_f('fun1 {x}')
+       >>> cry_f('fun2 {y}')
+       'fun2 (fun1 (1 : [7]))'
+    """
+    return CryptolTerm(to_cryptol_str_customf(s, frames=1))
 
-def array(*elements: SetupVal) -> ArrayVal:
+def array(*elements: SetupVal) -> SetupVal:
     """Returns an array with the provided ``elements`` (i.e., an ``ArrayVal``).
 
     N.B., one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out.
@@ -647,7 +678,7 @@ def array(*elements: SetupVal) -> ArrayVal:
             raise ValueError('array expected a SetupVal, but got {e!r}')
     return ArrayVal(list(elements))
 
-def elem(base: SetupVal, index: int) -> ElemVal:
+def elem(base: SetupVal, index: int) -> SetupVal:
     """Returns the value of the array element at position ``index`` in ``base`` (i.e., an ``ElemVal``).
 
     Can also be created by using an ``int`` indexing key on a ``SetupVal``: ``base[index]``."""
@@ -657,7 +688,7 @@ def elem(base: SetupVal, index: int) -> ElemVal:
         raise ValueError('elem expected an int, but got {index!r}')
     return ElemVal(base, index)
 
-def field(base : SetupVal, field_name : str) -> FieldVal:
+def field(base : SetupVal, field_name : str) -> SetupVal:
     """Returns the value of struct ``base``'s field ``field_name`` (i.e., a ``FieldVal``).
 
     Can also be created by using a ``str`` indexing key on a ``SetupVal``: ``base[field_name]``."""
@@ -667,17 +698,17 @@ def field(base : SetupVal, field_name : str) -> FieldVal:
         raise ValueError('field expected a str, but got {field_name!r}')
     return FieldVal(base, field_name)
 
-def global_initializer(name: str) -> GlobalInitializerVal:
+def global_initializer(name: str) -> SetupVal:
     """Returns the initializer value of a named global ``name`` (i.e., a ``GlobalInitializerVal``)."""
     if not isinstance(name, str):
         raise ValueError('global_initializer expected a str naming a global value, but got {name!r}')
     return GlobalInitializerVal(name)
 
-def null() -> NullVal:
+def null() -> SetupVal:
     """Returns a null pointer value (i.e., a ``NullVal``)."""
     return NullVal()
 
-def struct(*fields : SetupVal) -> StructVal:
+def struct(*fields : SetupVal) -> SetupVal:
     """Returns an LLVM structure value with the given ``fields`` (i.e., a ``StructVal``)."""
     for field in fields:
         if not isinstance(field, SetupVal):
diff --git a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
index 6b0f1232d7..8715ac4524 100755
--- a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
+++ b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
@@ -2,6 +2,7 @@
 import os
 import os.path
 from saw_client import *
+from saw_client.crucible import cry, cry_f
 from saw_client.llvm import Contract, cry, cry_f, array_ty, alias_ty, i8, i32, i64
 from saw_client.proofscript import yices, ProofScript
 from cryptol import cryptoltypes
@@ -39,16 +40,16 @@ def alloc_blob(spec, n):
     p = spec.alloc(type=blob_type, read_only=True)
     datap = alloc_bytes(spec, n)
     spec.points_to(llvm.field(p, "data"), datap)
-    spec.points_to(llvm.field(p, "size"), llvm.cry_f("`{n}:[32]"))
-    spec.points_to(llvm.field(p, "allocated"), llvm.cry("0:[32]"))
-    spec.points_to(llvm.field(p, "growable"), llvm.cry("0:[8]"))
+    spec.points_to(llvm.field(p, "size"), cry_f("`{n}:[32]"))
+    spec.points_to(llvm.field(p, "allocated"), cry("0:[32]"))
+    spec.points_to(llvm.field(p, "growable"), cry("0:[8]"))
     return (p, datap)
 
 def alloc_blob_readonly(spec, n):
     p = spec.alloc(type=blob_type, read_only=True)
     datap = spec.alloc(array_ty(n, i8), read_only = True)
     spec.points_to(llvm.field(p, "data"), datap)
-    spec.points_to(llvm.field(p, "size"), llvm.cry_f("`{n}: [32]"))
+    spec.points_to(llvm.field(p, "size"), cry_f("`{n}: [32]"))
     return(p, datap)
 
 def alloc_init(spec, ty, v):
@@ -96,8 +97,8 @@ def __init__(self,n):
     def specification(self):
         (p, datap) = alloc_blob(self, self.n)
         self.execute_func(p)
-        self.points_to(datap, llvm.cry_f("zero:[{self.n}][8]"))
-        self.returns(llvm.cry("0:[32]"))
+        self.points_to(datap, cry_f("zero:[{self.n}][8]"))
+        self.returns(cry("0:[32]"))
 
 class increment_drbg_counter_spec(Contract):
     def specification(self):
@@ -105,16 +106,16 @@ def specification(self):
         v = self.fresh_var(bytes_type(blocksize), "v")
         self.points_to(datap, v)
         self.execute_func(p)
-        self.points_to(datap, llvm.cry_f("split ((join {v}) +1): [{blocksize}][8]"))
-        self.returns(llvm.cry("0:[32]"))
+        self.points_to(datap, cry_f("split ((join {v}) +1): [{blocksize}][8]"))
+        self.returns(cry("0:[32]"))
 
 class bytes_used_spec(Contract):
     def specification(self):
         (sp, keyp, s) = drbg_state(self,"drbg")
-        bytes_used = alloc_init(self, i64, llvm.cry("0:[64]"))
+        bytes_used = alloc_init(self, i64, cry("0:[64]"))
         self.execute_func(sp, bytes_used)
-        self.points_to(bytes_used, llvm.cry_f("{s}.bytes_used"))
-        self.returns(llvm.cry("0:[32]"))
+        self.points_to(bytes_used, cry_f("{s}.bytes_used"))
+        self.returns(cry("0:[32]"))
 
 class block_encrypt_spec(Contract):
     def specification(self):
@@ -122,8 +123,8 @@ def specification(self):
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", bytes_type(blocksize))
         outp = alloc_bytes(self, blocksize)
         self.execute_func(keyp, msgp, outp)
-        self.points_to(outp, llvm.cry_f("encrypt_128 {key} {msg}"))
-        self.returns(llvm.cry("0 : [32]"))
+        self.points_to(outp, cry_f("encrypt_128 {key} {msg}"))
+        self.returns(cry("0 : [32]"))
 
 class encryptUpdate_spec(Contract):
     def __init__(self,n):
@@ -134,12 +135,12 @@ def specification(self):
         # but it is constant in the DRBG cryptol specification.
         (key, keyp) = ptr_to_fresh_readonly(self, "key", ctx_type)
         outp = alloc_bytes(self, self.n)
-        lenp = alloc_init(self, i32, llvm.cry_f("{self.n} : [32]"))
+        lenp = alloc_init(self, i32, cry_f("{self.n} : [32]"))
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", (bytes_type(self.n)))
-        self.execute_func(keyp, outp, lenp, msgp, llvm.cry_f("`{blocksize} : [32]"))
-        self.points_to(outp, llvm.cry_f("encrypt_128 {key} {msg}"))
-        self.points_to(lenp, llvm.cry_f("{self.n} : [32]"))
-        self.returns (llvm.cry("1 : [32]"))
+        self.execute_func(keyp, outp, lenp, msgp, cry_f("`{blocksize} : [32]"))
+        self.points_to(outp, cry_f("encrypt_128 {key} {msg}"))
+        self.points_to(lenp, cry_f("{self.n} : [32]"))
+        self.returns (cry("1 : [32]"))
 
 class bits_spec(Contract):
     def __init__(self, n):
@@ -151,16 +152,16 @@ def specification(self):
         self.execute_func(sp, outp)
         res = cry_f("drbg_generate_internal `{{n={self.n}*8}} {s}")
         # Remove some of the parens here to get really bad error messages
-        c = llvm.cry("split (({res}).0) : [{self.n}][8]")
+        c = cry("split (({res}).0) : [{self.n}][8]")
         self.points_to(datap, c)
         ensure_drbg_state(self, sp, keyp, cry_f("{res}.1"))
-        self.returns (llvm.cry(" 0 : [32] "))
+        self.returns (cry(" 0 : [32] "))
 
 def ensure_drbg_state(spec, p, keyp, s):
-    spec.points_to(llvm.field(p, "bytes_used"), llvm.cry_f("{s}.bytes_used"))
+    spec.points_to(llvm.field(p, "bytes_used"), cry_f("{s}.bytes_used"))
     spec.points_to(llvm.field(p, "ctx"), keyp)
-    spec.points_to(keyp, llvm.cry_f("split ({s}.ctx.key) : [{keysize}][8]"))
-    spec.points_to(llvm.field(p, "v"), llvm.cry_f("split ({s}.v) : [{blocksize}][8]"))
+    spec.points_to(keyp, cry_f("split ({s}.ctx.key) : [{keysize}][8]"))
+    spec.points_to(llvm.field(p, "v"), cry_f("split ({s}.v) : [{blocksize}][8]"))
     mixes = spec.fresh_var(i64, "mixes")
     spec.points_to(llvm.field(p, "mixes"), mixes)
 
@@ -203,15 +204,15 @@ class cipher_cleanup_spec(Contract):
     def specification(self):
         ctx = self.alloc(ctx_type)
         self.execute_func(ctx)
-        self.points_to(ctx, llvm.cry_f("zero : [{keysize}][8]"))
-        self.returns(llvm.cry("1:[32]"))
+        self.points_to(ctx, cry_f("zero : [{keysize}][8]"))
+        self.returns(cry("1:[32]"))
 
 class cipher_key_length_spec(Contract):
     def specification(self):
         ctx = self.alloc(ctx_type, read_only = True)
         self.execute_func(ctx)
         # Specialized to AES-128 for now
-        self.returns(llvm.cry("16:[32]"))
+        self.returns(cry("16:[32]"))
 
 class encryptInit_spec(Contract):
     def specification(self):
@@ -224,7 +225,7 @@ def specification(self):
         #self.execute_func(ctx, stp, llvm.null, keyp, llvm.null)
         self.execute_func(ctx, llvm.null, llvm.null, keyp, llvm.null)
         self.points_to(ctx, key)
-        self.returns(llvm.cry("1:[32]"))
+        self.returns(cry("1:[32]"))
 
 class get_public_random_spec(Contract):
     def __init__(self):
@@ -234,8 +235,8 @@ def specification(self):
         (p, datap) = alloc_blob(self, seedsize)
         self.execute_func(p)
         # TODO: blocked on 'fake_entropy'
-        #self.points_to(datap, llvm.cry_f("split fake_entropy : [{seedsize}][8]"))
-        self.returns(llvm.cry("0: [32]"))
+        #self.points_to(datap, cry_f("split fake_entropy : [{seedsize}][8]"))
+        self.returns(cry("0: [32]"))
 
 class supports_rdrand_spec(Contract):
     def specification(self):
@@ -274,7 +275,7 @@ def specification(self):
         self.points_to(datap, data)
         self.execute_func(sp, providedp)
         ensure_drbg_state(self, sp, keyp, "drbg_update (join {data}) ({s})".format(data=data.name(), s=s))
-        self.returns(llvm.cry("0:[32]"))
+        self.returns(cry("0:[32]"))
 
 class seed_spec(Contract):
     def __init__(self, n):
@@ -289,7 +290,7 @@ def specification(self):
         expr = "drbg_reseed ({s}) (fake_entropy) (join ({data}))".format(s=s,
                 data=data.name())
         ensure_drbg_state(self, sp, keyp, expr)
-        self.returns(llvm.cry("0:[32]"))
+        self.returns(cry("0:[32]"))
 
 zero_ov_block = llvm_verify(mod, 's2n_blob_zero', blob_zero_spec(blocksize))
 zero_ov_seed = llvm_verify(mod, "s2n_blob_zero", blob_zero_spec(seedsize))
diff --git a/saw-remote-api/python/tests/saw/test_alloc_aligned.py b/saw-remote-api/python/tests/saw/test_alloc_aligned.py
index 22e11360b2..e1881e14ce 100644
--- a/saw-remote-api/python/tests/saw/test_alloc_aligned.py
+++ b/saw-remote-api/python/tests/saw/test_alloc_aligned.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, FreshVar, SetupVal, cry, cry_f, struct, LLVMType, array_ty, i8, i64
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, FreshVar, SetupVal, struct, LLVMType, array_ty, i8, i64
 from typing import Tuple
 
 
diff --git a/saw-remote-api/python/tests/saw/test_basic_java.py b/saw-remote-api/python/tests/saw/test_basic_java.py
index 43ba2bda26..a4ab2be61d 100644
--- a/saw-remote-api/python/tests/saw/test_basic_java.py
+++ b/saw-remote-api/python/tests/saw/test_basic_java.py
@@ -3,7 +3,8 @@
 
 import saw_client as saw
 
-from saw_client.jvm import Contract, java_int, cry, cry_f
+from saw_client.crucible import cry, cry_f
+from saw_client.jvm import Contract, java_int
 
 class Add(Contract):
     def __init__(self) -> None:
diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py
index a9a05e4a6b..c88b11832f 100644
--- a/saw-remote-api/python/tests/saw/test_ghost.py
+++ b/saw-remote-api/python/tests/saw/test_ghost.py
@@ -1,5 +1,6 @@
 import saw_client as saw
-from saw_client.llvm import Contract, CryptolTerm, cry, cry_f, void, i32, GhostVariable
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, CryptolTerm, void, i32, GhostVariable
 
 import unittest
 from pathlib import Path
diff --git a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
index c56d21fa4f..c48055023e 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cry, cry_f, null, i32
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, null, i32
 
 
 class FContract1(Contract):
diff --git a/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py b/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
index 8cb94fa36e..0045ce6a62 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, FreshVar, LLVMType, SetupVal, array_ty, cry, cry_f, i64, void
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, FreshVar, LLVMType, SetupVal, array_ty, i64, void
 from saw_client.option import LaxPointerOrdering
 
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_pointer.py b/saw-remote-api/python/tests/saw/test_llvm_pointer.py
index 01ccb9113f..3721a18a7a 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_pointer.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_pointer.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cry, cry_f, void, i8, ptr_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, void, i8, ptr_ty
 
 
 class FContract(Contract):
diff --git a/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
index 96d6dfcec9..c8c7bf2ade 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, LLVMIntType, alias_ty, cry, cry_f, i8, void
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, LLVMIntType, alias_ty, i8, void
 from saw_client.option import LaxLoadsAndStores
 
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct.py b/saw-remote-api/python/tests/saw/test_llvm_struct.py
index 8702782de5..66eca1cf3c 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_struct.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_struct.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, SetupVal, FreshVar, cry, cry_f, struct, LLVMType, void, array_ty, i32, alias_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, SetupVal, FreshVar, struct, LLVMType, void, array_ty, i32, alias_ty
 
 
 def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]:
diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
index 8c552f474a..6c1679e96d 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cry, cry_f, struct, void, i32, array_ty, struct_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, struct, void, i32, array_ty, struct_ty
 
 
 class FContract(Contract):
diff --git a/saw-remote-api/python/tests/saw/test_points_to_at_type.py b/saw-remote-api/python/tests/saw/test_points_to_at_type.py
index 577250cfb8..e072ccb609 100644
--- a/saw-remote-api/python/tests/saw/test_points_to_at_type.py
+++ b/saw-remote-api/python/tests/saw/test_points_to_at_type.py
@@ -2,7 +2,8 @@
 import unittest
 from saw_client import *
 from saw_client.exceptions import VerificationError
-from saw_client.llvm import Contract, LLVMType, PointerType, cry, cry_f, void, i32, array_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, LLVMType, PointerType, void, i32, array_ty
 from typing import Union
 
 
diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py
index f2d13f96e7..29cca88576 100644
--- a/saw-remote-api/python/tests/saw/test_salsa20.py
+++ b/saw-remote-api/python/tests/saw/test_salsa20.py
@@ -2,7 +2,8 @@
 import unittest
 from cryptol.cryptoltypes import to_cryptol
 from saw_client import *
-from saw_client.llvm import Contract, void, SetupVal, FreshVar, cry, cry_f, i8, i32, LLVMType, LLVMArrayType
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, void, SetupVal, FreshVar, i8, i32, LLVMType, LLVMArrayType
 from saw_client.proofscript import z3
 
 

From 53f106f974ef6c51dd529240a0bd7caeba242f28 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Fri, 24 Dec 2021 12:02:20 -0800
Subject: [PATCH 8/9] whoops, fix imports in drbg.py

---
 saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
index 8715ac4524..435ad18110 100755
--- a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
+++ b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
@@ -3,7 +3,7 @@
 import os.path
 from saw_client import *
 from saw_client.crucible import cry, cry_f
-from saw_client.llvm import Contract, cry, cry_f, array_ty, alias_ty, i8, i32, i64
+from saw_client.llvm import Contract, array_ty, alias_ty, i8, i32, i64
 from saw_client.proofscript import yices, ProofScript
 from cryptol import cryptoltypes
 #from saw.dashboard import Dashboard

From 4705427c584cf0fe0f63bdd2b29eb81e9edac5e0 Mon Sep 17 00:00:00 2001
From: Andrew Kent <andrew@galois.com>
Date: Mon, 3 Jan 2022 13:59:50 -0800
Subject: [PATCH 9/9] Update saw-remote-api/python/saw_client/crucible.py

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
---
 saw-remote-api/python/saw_client/crucible.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index 16c5d7a385..5d5ff39a0c 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -643,7 +643,7 @@ def cry_f(s : str) -> CryptolTerm:
        and ``cry_f('{{ x = {x} }}')`` is equal to ``cry('{ x = [0,1] }')``.
 
        When formatting Cryptol, it is recomended to use this function rather
-       than any of python's built-in methods of string formatting (e.g.
+       than any of Python's built-in methods of string formatting (e.g.
        f-strings, ``str.format``) as the latter will not always produce valid
        Cryptol syntax. Specifically, this function differs from these methods
        in the cases of ``BV``s, string literals, function application (this