search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

Injective mapping from Cryptol types into saw-core #1613

Open brianhuffman opened 2 years ago

brianhuffman commented 2 years ago

Currently the Cryptol to saw-core translation conflates some types: Tuple types are represented as nested right-associative pairs, so e.g. (a, b, c) and (a, (b, c)) are both translated as the same type a * b * c. Also, Cryptol record types are simply converted to tuple types of the same size, so record field names are completely lost.

This causes some problems: For example, translated records are hard to make sense of because of the missing field names (#878). Also, it's currently not possible to reliably recover a cryptol type given a saw-core term (#718).

We need a new encoding of tuple and record types into saw-core that is injective, so that we don't lose information translating from Cryptol to saw-core. Also, to improve the user experience with saw-core, we should make tuples and records look, feel, and behave the same way they do in Cryptol (as much as possible).

brianhuffman commented 2 years ago

PR #1612 is a step in this direction.