Support importing Cryptol enums into SAWCore

[RyanGlScott]

The Need

Since #2020, SAW bundles a version of Cryptol that includes support for Cryptol's enum declarations. It it still not possible to import Cryptol files that define enums into SAWCore, however. For example, given this Cryptol and SAW file:

// Test.cry
enum Foo = MkFoo

// test.saw
import "Test.cry";

If you run test.saw, it will throw an error message:

$ ~/Software/saw-1.1/bin/saw test.saw
[13:24:15.614] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[13:24:15.634] genNominalConstrurctors: `enum` is not yet supported
CallStack (from HasCallStack):
  error, called at src/Verifier/SAW/Cryptol.hs:2034:22 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol

Alternatively, you might also see this error message if you load a program which uses (but does not define) an enum:

// Test.cry

f : Option () -> ()
f x =
  case x of
    None -> ()
    Some y -> y

$ ~/Software/saw-1.1/bin/saw test.saw
[13:25:05.093] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[13:25:05.113] importType: `enum` is not yet supported
CallStack (from HasCallStack):
  error, called at src/Verifier/SAW/Cryptol.hs:274:25 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol

This issue tracks lifting this restriction.

Design Choices, Elaborated

The major design choice here for the translation of enums into SAWCore is to pick one of

1. Map each Cryptol enum declaration to a SAWCore data declaration with the same field types.
2. Map each Cryptol enum declaration to a value defined in terms of Eithers, which provides an "anonymous sum" representation.

Discussion on design choice

• Choice 1

  • pro: Seems the most elegant.
  • pro: generated code will be more constrained by the SAWCore type system, this may make code more robust.
  • con: Requires more understanding of more code. The current translation code assumes we are only adding definitions, not "type/nominal declarations" (which affect the environment more substantially than adding a single definition). The relevant environments seem numerous and somewhat redundant and some are "under" IORefs.
  • con: the syntax and semantics of the SAWCore language is not documented: one must read the examples, and the source code, one needs to figure out recursors and etc. Makes this choice a little more effort!
  • pro: the type conversion is injective (two distinct cryptol types will not map to the same SAWCore types)
  • pro: it may be more efficient as we expect to have a single case "branch".

• Choice 2

  • pro: quickest to implement, less code that needs to be understood and modified.

For now we are proceeding with design Choice 2, when possible, abstracting over aspects that would change under Choice 1.

Implementation and progress

• fixed the Fixing nominals in cryptol lib bug (solving #2230) #2233 bug.

• learning the Cryptol, SawCore, and translation ('cryptol-saw-core') code.

• All (or most all) the changes will be in cryptol-saw-core/src/Verifier/SAW/Cryptol.hs:

  • creating constructors and adding to the environment when we process the enum declaration.
    • various design choices made here: e.g., we add constructors to the environment (thus not duplicating constructor code)
    • partially implemented
    • testing and modifications in progress.
  • translating Cryptol constructors inside Cryptol Expressions.
  • translating the Cryptol enum type to the desired SAWCore type.
  • translating case expressions from Cryptol into SAWCore.
  • Optional: exporting Values? not fully implemented for other types, so ...?

• Add tests.

Further Steps & Improvements

• As discussed, above it would be an improvement to map the enum types injectively into a new, unique type in Saw. This appears to need a bit more restructuring to implement. Were we to go this route, refer to the "code path" thatload_sawcore_from_file follows (on saw command-line). This processes SAWCore data declarations.
• A further step would be to allow using Cryptol enums in MIR specifications, as proposed in Allow more MIR types to be "flexibly" embedded into Cryptol #1976.)

[RyanGlScott]

It is also possible to make SAW outright panic by using an enum in the return type of a function:

// Test.cry

f : Option ()
f = None

$ ~/Software/saw-1.1/bin/saw test.saw
[13:33:52.133] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[13:33:52.155] You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues

%< --------------------------------------------------- 
  Revision:  5c16c876f35f0abdf0b412a5387e220b15b7f990
  Branch:    release-1.1 (uncommited files present)
  Location:  importExpr
  Message:   unknown variable: Name {nUnique = 4188, nInfo = GlobalName UserName (OrigName {ogNamespace = NSConstructor, ogModule = TopModule (ModName "Cryptol" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "None", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 645, col = 17}, to = Position {line = 645, col = 21}, source = "/home/ryanscott/Software/saw-1.1/lib/Cryptol.cry"}}
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1081:25 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol
%< ---------------------------------------------------

It's not obvious to me if it is straightforward to fix this panic without doing all of the necessary legwork to support enums wholesale, but I thought I'd mention it here as well.

---

@mtullsen says: this part of the picture is actually solved in #2230.