[Remote API] property introspection?

[WeeknightMVP]

Given a loaded module M and a name n, how can one apply the Cryptol Remote API for Python to determine whether n is a property, and which module in scope defines it?

// test_names/P.cry
module P where
  n: [32] -> Bool
  property n x = and x \/ (x + 1 > x)

// test_names/M.cry
module M where
  import P (n)

In the Cryptol REPL, :browse reports this information:

$ export CRYPTOLPATH=$(pwd)/test_names
$ cat test_names/P.cry
// test_names/P.cry
module P where
  n: [32] -> Bool
  property n x = and x \/ (x + 1 > x)
$ cat test_names/M.cry
// test_names/M.cry
module M where
  import P (n)
$ cd cryptol
cryptol$ git pull
...
cryptol$ ./cry run
...
Cryptol> :m M
Loading module Cryptol
Loading module P
Loading module M
M> :b
...

Properties
==========

  From P
  ------

    n : [32] -> Bool

...

However, CryptolConnection.names() in the Cryptol Remote API for Python does not:

cryptol$ export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api)
cryptol$ cd ../test_names
test_names$ cat pyproject.toml
...
[tool.poetry.dependencies]
python = "^3.10"
cryptol = {path = "../cryptol/cryptol-remote-api/python"}
...
test_names$ poetry shell
...
test_names$ python3
...
>>> from pprint import pprint
>>> from cryptol import connect
>>> c = connect(reset_server=True)
>>> m = c.load_module()
>>> names = c.names()
>>> n = next(x for x in names if x['name'] == 'n')
>>> pprint(n)
{'name': 'n',
 'type': {'forall': [],
          'propositions': [],
          'type': {'domain': {'type': 'bitvector',
                              'width': {'type': 'number', 'value': 32}},
                   'range': {'type': 'Bit'},
                   'type': 'function'}},
 'type string': '[32] -> Bit'}

One could infer from n's type (or type string) (... -> Bit) that it could be a property, but this pragma clearly distinguishes predicates intended to be verified (:proven or :checked) -- i.e. those that express when definitions are valid -- from those used in a module's implementation (e.g. all, and, elem, etc.). It is possible to collect this information by parsing a process interaction with the REPL (e.g. using pexpect), but this seems counterproductive.

[RyanGlScott]

Indeed, this is something that simply isn't included in the remote API. In principle, we should be able to add a property : bool field to represent this.

[RyanGlScott]

@yav points out that property is a specific type of Cryptol pragma, so we should make a general-purpose Pragma class in the Python API (especially if we need to extend it in the future).

[m-yac]

I believe this is fixed in #1512: In that PR, any property n in names() will now satisfy 'pragmas' in n and 'property' in n['pragmas']. That PR also adds property_names(), which filters names() to include only those such names.