SAWCore read/write primitives fail with polymorphic terms

[ChrisEPhifer]

Consider the following SAWScript:

let t = {{ \x -> x }};
write_core "t.out" t;
t_in <- read_core "t.out";

This script panics at read_core with the following from cryptol-verifier:

%< --------------------------------------------------- 
  Revision:  315a6d201bbc002bb5e414945e885db5d9958444
  Branch:    HEAD
  Location:  scCryptolType
  Message:   scCryptolType: unsupported type (u911 : sort 0)
-> (x : u911)
-> u911
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-verifier-0.1-aALHfjF4GzKez0Qlpznm1:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1158:19 in cryptol-verifier-0.1-aALHfjF4GzKez0Qlpznm1:Verifier.SAW.Cryptol
%< --------------------------------------------------- 

This appears to be an issue with the use of Cryptol within SAW, rather than with Cryptol itself.

[ChrisEPhifer]

Note: This fails for terms of non-arrow types as well, e.g.

let t = {{ [1..10] }};
write_core "t.out" t;
t_in <- read_core "t.out";

Fails in exactly the same way as the example above.

[brianhuffman]

The read_core primitive is implemented using function scCryptolType, which I've been trying to get rid of (see #718). If we want to be able to read and write saw-script Term values to external core files, we'll have to come up with a better way to reliably save and restore the Cryptol type of the term. Not only does scCryptolType crash sometimes, neither is it guaranteed to come back with the same type you started with.

To fix this, I think we might have to augment the external core format with some extra type information.

[WeeknightMVP]

Here's a script demonstrating some more write_core/read_core misbehavior:

let filename = "core.txt";

let test (label: String) (t: Term): TopLevel () = do {
    print (str_concat (str_concat "Test `" label) "`:");

    print "t: "; print t;
    print "type t: "; print (type t);

    print (str_concat (str_concat "Writing `t` to `" filename) "`...");
    write_core filename t;

    print (str_concat (str_concat "Reading `t'` from `" filename) "`...");
    t' <- read_core filename;

    print "t': "; print t';
    print "type t': "; print (type t');
    print "t == t'? "; print (eval_bool {{ t' == t }});

    print "";
    print "";
};

let main: TopLevel () = do {
    print "Testing `write_core` ... `read_core` recovery...";

    let test1 = test "Record"         {{ { s20_crypt32 = [ 63, 64, 65 : Integer ], s20_expand32 = [ () ] } }};
    let test2 = test "List of Tuples" {{ [ (11, "s20_crypt32 "), (12, "s20_expand32") ] }};
    let test3 = test "Tuple"          {{ (0, [ 63, 64, 65 : Integer ]) }};

    fails test1;  // 17: inconsistent types (record demotion to tuple)
    fails test2;  // 13: `read_core` encounters bug in `cryptol-saw-core`
    fails test3;  // 13: `read_core` encounters bug in `cryptol-saw-core`
};

[sauclovian-g]

This is related to #2119 and #659 (all involve the handling of Cryptol types in saw-core) so there's probably a comprehensive solution to be had.