Skip to content

selector syntax regression #926

@robdockins

Description

@robdockins

Recent changes in the selector syntax seem to have broken some previous code. This is from the saw-script repository, in the example ECDSA verification.

https://github.com/GaloisInc/saw-script/blob/6247f9ac936628cb6f9e74f33738e059eb32582b/examples/ecdsa/cryptol-spec/p384_ec_mul.cry#L212

Maybe we accidentally removed prime characters from the lexical syntax for selectors?

$ ./cry run ~/code/saw-script/examples/ecdsa/cryptol-spec/p384_ec_mul.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.9.1.99 (96fcce9, modified)
https://cryptol.net  :? for help

Parse error at /Users/rdockins/code/saw-script/examples/ecdsa/cryptol-spec/p384_ec_mul.cry:212:35--212:44
  malformed selector: .tma2_c0'

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething not working correctlyparserIssues with lexing or parsing.

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions