Printing of Cryptol newtypes in counterexamples throws away too much information

[sauclovian-g]

If your model has a Cryptol newtype in it (recall that newtypes are records) it gets embedded into saw-core as a tuple and throws away the record field names. This translation, however, also throws away the field ordering; the fields get sorted alphabetically before or during the translation.

The result of this is that when a counterexample containing a newtype gets printed, it comes out as a tuple of unlabeled values whose order does not (in general) match the original declaration. Once you realize what's going on, it's possible to sort this out by hand. It's not reasonable to expect the user to do that though, and also before you figure out what's going on the results are just incomprehensible.

It's not clear to me if we ought to throw away less information when translating to saw-core (that is, add record types and maybe other things to saw-core, which is a fairly big deal) or if this ought to get fixed by introducing a mechanism to lift saw-core counterexample values back to their source-level language. (That is also likely a fairly big deal, because it almost certainly involves substantial structural changes, and might still also require carrying more information around in saw-core.)

However, I think something needs to be done about it.

[RyanGlScott]

For a specific example of this in action, run the following SAW script:

// Test.cry
newtype T = { x : [16], y : [32] }

// test.saw
import "Test.cry";
prove_print z3 {{ \(t : T) -> False }};

$ ~/Software/saw-1.2/bin/saw test.saw
[16:22:21.150] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[16:22:21.225] Stack trace:
"prove_print" (/home/ryanscott/Documents/Hacking/SAW/test.saw:3:1-3:12)
prove: 1 unsolved subgoal(s)
Invalid: [t = (0, 0)]

Note that the counterexample is printed as t = (0, 0) rather than something like t = T { x = 0, y = 0 }.

[RyanGlScott]

Cryptol also suffers from the same problem, but in a more limited context. This is because when Cryptol typechecks newtypes, it throws away the name of the newtype and treats it the same as any record. For example, if you try proving this in the Cryptol REPL (after loading Test.cry above):

$ ~/Software/cryptol-3.2.0/bin/cryptol Test.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.2.0 (1bcb75c)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
Main> :prove \(x : T) -> False
Counterexample
(\(x : T) -> False) {x = 0x0000, y = 0x00000000} = False
(Total Elapsed Time: 0.016s, using "Z3")

Then the counterexample is printed as a value of type {x : [16], y : [32]} rather than as a value of type T.

[sauclovian-g]

I've seen that, and I don't think I ever noticed the missing T. FWIW.

Does that mean SAW gets the type as a plain record without the newtype name?

[RyanGlScott]

Does that mean SAW gets the type as a plain record without the newtype name?

I'm a bit fuzzy on the details, but I believe that after Cryptol's typechecking phase, newtype values look exactly like record values. That being said, I do believe that the distinction between newtype types and record types is kept, given that we record the existence of newtypes in the post-typechecked AST (here).