`yosys_import` can create invalid Cryptol field names

[podhrmic]

yosys_import currently accepts any string in the cell name, even though it is not a valid Cryptol field name. For example "type": "full_default(fullarch)", in the JSON below is illegal. I can simply preprocess the JSON file, but wanted to raise this in case you wanted to at least throw an error/warning when importing illegal cell names into SAW.

Original comment from @RyanGlScott below:

Details

$ jq '.modules.["full_default(fullarch)"]' adder_tabby.json
{
  "attributes": {
    "architecture": "fullarch",
    "library": "work",
    "hdlname": "full",
    "src_entity": "adder.vhd:22.8-22.12",
    "src": "adder.vhd:32.14-32.22"
  },
  "ports": {
    "a": {
      "direction": "input",
      "bits": [
        2
      ]
    },
    "b": {
      "direction": "input",
      "bits": [
        3
      ]
    },
    "cin": {
      "direction": "input",
      "bits": [
        4
      ]
    },
    "cout": {
      "direction": "output",
      "bits": [
        5
      ]
    },
    "s": {
      "direction": "output",
      "bits": [
        6
      ]
    }
  },
  "cells": {
    "$verific$i4$adder.vhd:39$32": {
      "hide_name": 1,
      "type": "$or",
      "parameters": {
        "A_SIGNED": "00000000000000000000000000000000",
        "A_WIDTH": "00000000000000000000000000000001",
        "B_SIGNED": "00000000000000000000000000000000",
        "B_WIDTH": "00000000000000000000000000000001",
        "Y_WIDTH": "00000000000000000000000000000001"
      },
      "attributes": {
        "src": "adder.vhd:39.11-39.27"
      },
      "port_directions": {
        "A": "input",
        "B": "input",
        "Y": "output"
      },
      "connections": {
        "A": [
          7
        ],
        "B": [
          8
        ],
        "Y": [
          9
        ]
      }
    },
    "$verific$i5$adder.vhd:39$33": {
      "hide_name": 1,
      "type": "$_BUF_",
      "parameters": {},
      "attributes": {},
      "port_directions": {
        "A": "input",
        "Y": "output"
      },
      "connections": {
        "A": [
          9
        ],
        "Y": [
          5
        ]
      }
    },
    "half0": {
      "hide_name": 0,
      "type": "half_default(halfarch)",
      "parameters": {},
      "attributes": {
        "src": "adder.vhd:37.3-37.8"
      },
      "port_directions": {
        "a": "input",
        "b": "input",
        "c": "output",
        "s": "output"
      },
      "connections": {
        "a": [
          2
        ],
        "b": [
          3
        ],
        "c": [
          7
        ],
        "s": [
          10
        ]
      }
    },
    "half1": {
      "hide_name": 0,
      "type": "half_default(halfarch)",
      "parameters": {},
      "attributes": {
        "src": "adder.vhd:38.3-38.8"
      },
      "port_directions": {
        "a": "input",
        "b": "input",
        "c": "output",
        "s": "output"
      },
      "connections": {
        "a": [
          10
        ],
        "b": [
          4
        ],
        "c": [
          8
        ],
        "s": [
          6
        ]
      }
    }
  },
  "netnames": {
    "$verific$half0$adder.vhd:37$24": {
      "hide_name": 1,
      "bits": [
        11
      ],
      "attributes": {}
    },
    "$verific$half0$adder.vhd:37$25": {
      "hide_name": 1,
      "bits": [
        12
      ],
      "attributes": {}
    },
    "$verific$half0$adder.vhd:37$26": {
      "hide_name": 1,
      "bits": [
        13
      ],
      "attributes": {}
    },
    "$verific$half0$adder.vhd:37$27": {
      "hide_name": 1,
      "bits": [
        14
      ],
      "attributes": {}
    },
    "$verific$half1$adder.vhd:38$28": {
      "hide_name": 1,
      "bits": [
        15
      ],
      "attributes": {}
    },
    "$verific$half1$adder.vhd:38$29": {
      "hide_name": 1,
      "bits": [
        16
      ],
      "attributes": {}
    },
    "$verific$half1$adder.vhd:38$30": {
      "hide_name": 1,
      "bits": [
        17
      ],
      "attributes": {}
    },
    "$verific$half1$adder.vhd:38$31": {
      "hide_name": 1,
      "bits": [
        18
      ],
      "attributes": {}
    },
    "$verific$n12$23": {
      "hide_name": 1,
      "bits": [
        9
      ],
      "attributes": {}
    },
    "a": {
      "hide_name": 0,
      "bits": [
        2
      ],
      "attributes": {
        "src": "adder.vhd:24.5-24.6"
      }
    },
    "b": {
      "hide_name": 0,
      "bits": [
        3
      ],
      "attributes": {
        "src": "adder.vhd:25.5-25.6"
      }
    },
    "cin": {
      "hide_name": 0,
      "bits": [
        4
      ],
      "attributes": {
        "src": "adder.vhd:26.5-26.8"
      }
    },
    "cout": {
      "hide_name": 0,
      "bits": [
        5
      ],
      "attributes": {
        "src": "adder.vhd:27.5-27.9"
      }
    },
    "half0c": {
      "hide_name": 0,
      "bits": [
        7
      ],
      "attributes": {
        "src": "adder.vhd:33.10-33.16"
      }
    },
    "half0s": {
      "hide_name": 0,
      "bits": [
        10
      ],
      "attributes": {
        "src": "adder.vhd:34.10-34.16"
      }
    },
    "half1c": {
      "hide_name": 0,
      "bits": [
        8
      ],
      "attributes": {
        "src": "adder.vhd:35.10-35.16"
      }
    },
    "s": {
      "hide_name": 0,
      "bits": [
        6
      ],
      "attributes": {
        "src": "adder.vhd:28.5-28.6"
      }
    }
  }
}

This doesn't cause cause problems for the yosys_import command per se, but it does result in a Term with Cryptol fields that have inaccessible names:

sawscript> m <- yosys_import "adder_tabby.json"
sawscript> print (type m)
[19:56:59.559] {add4 : {a : [4], b : [4]} -> {res : [4]},
 full_default(fullarch) : {a : [1], b : [1], cin : [1]} ->
 {cout : [1], s : [1]},
 half_default(halfarch) : {a : [1], b : [1]} -> {c : [1], s : [1]}}
sawscript> print (type {{ m.full_default(fullarch) }})

Stack trace:
   (builtin) (at top level)
Cryptol error:
[error] at <stdin>:1:31--1:39
    Value not in scope: fullarch

Perhaps we should escape characters with special meaning in Cryptol, such as parentheses?

[sauclovian-g]

Do we need a solution that provides a representation for every character out there, or is there a limited set that can appear?

[RyanGlScott]

I don't have a keen sense for what special characters TabbyCAD is likely to produce, but it probably wouldn't hurt to ensure that all special characters are encoded somehow. By "special characters", I mean any character that isn't allowed in a valid Cryptol identifier, i.e.,

@id_first     = [a-zA-Z_] | $unilower | $uniupper
@id_next      = [a-zA-Z0-9_'] | $unilower | $uniupper | $unidigit | $unitick

@id           = @id_first @id_next*

[podhrmic]

Looks like TabbyCAD is willing to create pretty wild names, for example:

...
"type": "\\\\aes_gcm(aes_gcm_mode_g=\"00\",aes_gcm_n_rounds_g=1)\\(arch_aes_gcm)",
...

Ideally we would filter all illegal characters.

[brianhuffman]

Do we need a mapping from JSON strings to field names that is injective? Or is it enough to avoid field-name collisions within the same datatype?

Also, there are some otherwise-lexically-valid strings that won't work as Cryptol field names because they are reserved keywords, e.g. where. Should we do extra work to avoid reserved names?

[RyanGlScott]

I think turning full_default(fullarch) into something like full_default40fullarch41 (where 40 and 41 are the ASCII equivalents of ( and ), respectively) should suffice. I suppose that there is a risk that another cell might literally be named full_default40fullarch41, but this seems pretty unlikely.

Should we do extra work to avoid reserved names?

Yes, I think that's worth doing as well.

[sauclovian-g]

I was thinking about the following transform:

• encode illegal characters as ' followed by two hex digits (or do we need to allow four or eight?)
• encode an ' that appears in the middle of the name as ''
• leave alone all ' that appear at the end of the name
• if the name now begins with ', prefix that with h'm

This is injective, and is fairly easily encoded and decoded, and shouldn't be any more unsightly than necessary (e.g. full_default'40fullarch'41, h'm'5c'5caes_gcm'40aes_gcm_mode_g'3d'2200'22'2caes_gcm_n_rounds_g'3d1'41'5c'40arch_aes_gcm'41) not that it's great.

Another option is to use ' to switch from text into hex mode: full_default'40'fullarch'41' and h'm'5c5c'aes_gcm'40'aes_gcm_mode_g'3d22'00'222c'aes_gcm_n_rounds_g'3d'1'415c40'arch_aes_gcm'41' but this requires encoding trailing ', which isn't entirely desirable.

[sauclovian-g]

It also might make sense, since ultimately these names are going to end up in proofs and that's inherently going to suck, to instead allow the user to supply a mapping table that provides rationalized names.

Or we should make like the MIR backend does with Rust's indigestible identifiers and make a layer of indirection that supports lookup.

[RyanGlScott]

I don't have a strong opinion on what the naming conventions should be, provided that we document them.

allow the user to supply a mapping table that provides rationalized names

How are you envisioning this would work? An extremely simple solution would be to provide a list of (String, String) pairs, where the left String is the clunky autogenerated name, and the right String is an easier-to-type name. This approach would require that you figure out what the autogenerated names are in the first place, however, which somewhat defeats the point of having this convenience.

[podhrmic]

As a likely user, I am happy without the remapping - I think if I really cared about how the internal modules are named, I can just preprocess JSON with a sed script. So the easiest solution that makes SAW happy would be sufficient:-)

[sauclovian-g]

I think I was thinking in terms of match patterns of some kind, e.g. (.*)\((.*)\) -> \1_\2.

IDK, I'm not sure how many of these names will ever show up in anything user-facing. I'm just a little worried about the possibility of generating proof goals that are already mostly illegible for SAWCore reasons and then injecting a bunch of line noise into them.