Support property annotation

[weaversa]

It would be nice to know what functions in a Cryptol spec have the property annotation applied. Otherwise, we have to do something like below, and there no way to differentiate between properties and functions that return a bit.

from argo.connection import RemoteSocketProcess
from cryptol import connect, CryptolContext, CryptolFunctionHandle

from cihelper import check

c = connect(
    RemoteSocketProcess( 'localhost', 35553 ),
)

command = c.load_module('Primitive::Symmetric::Cipher::Stream::Salsa20')

ctx = CryptolContext(c)
fhs = [
    fh
    for attr in dir(ctx)
    if isinstance((fh := getattr(ctx, attr)), CryptolFunctionHandle)
]
bit_names = [
    name
    for fh in fhs
    if (
        fh.ty == 'Bit'
        and (name := fh.name) not in 'False True'
    )
]
ubf_names = [
    name
    for fh in fhs
    if (
        fh.ty.endswith('-> Bit')
        and fh.ty.find('->') == (len(fh.ty) - len('-> Bit'))
        and (name := fh.name) not in 'and or'
    )
]

for name in bit_names:
    check(c, name)

>>> ubf_names
['columnround_is_transpose_of_rowround', 'columnround_opt_is_columnround', 'littleendian_is_invertable', 'rowround_opt_is_rowround']
>>> bit_names
['Salsa20_passes_tests', 'columnround_passes_tests', 'doubleround_passes_tests', 'littleendian_passes_tests', 'quarterround_passes_tests', 'rowround_passes_tests']