Cryptol primitives can't be made uninterpreted

[brianhuffman]

Usually constants translated from Cryptol are eligible to be made uninterpreted with tactics like unint_z3. But it doesn't work if the constant is a cryptol primitive. For example:

sawscript> prove (unint_z3 ["complement"]) {{ \(x:[8]) y -> x == y ==> complement x == complement y }}

Stack trace:
"prove" (<stdin>:1:1-1:6):
"unint_z3" (<stdin>:1:8-1:16):
Could not resolve name: "complement"

The deeper problem is that the name "complement" is not registered under its proper name in saw-core, as other cryptol constants are. If we print the term, we can see that there is no trace of the original name:

sawscript> print_term {{ complement }}
[02:02:56.016] ecCompl

[brianhuffman]

My first attempt at this was to change the cryptol-saw-core translator to define an scConstant using the cryptol name for each translated primitive. However, it turns out that this breaks a lot of integration tests. One problem is that this makes rewriting with cryptol_ss pretty much useless, because the none of the rewrite rules in Cryptol.sawcore match anymore; those rewrite rules expect to match on the saw-core names, which are now hidden inside abstract constants.

Perhaps a better, less disruptive approach would simply be to rename all the constants in Cryptol.sawcore that implement cryptol primitives to use the exact same name as the cryptol primitive. Then cryptol_ss would still work, and using the cryptol name as an argument to unint_z3 would also work because the name is the same.

[brianhuffman]

I have a patch for renaming some of the primitives in Cryptol.sawcore now on the cryptol-prim-names branch.

[brianhuffman]

When this ticket is closed, we should also add the goal_eval_unint ["drop"] example from #1045 to our regression test suite.

[robdockins]

@brianhuffman, do you have idea/plans for this issue? I think #347 is now also basically an instance of this issue.

[brianhuffman]

Yes: My plan is to rename all the functions in Cryptol.sawcore so that every cryptol primitive is translated to a saw-core constant with the same name. However, this is blocked on #1258. We'll need to reimplement lexing and name resolution in the saw-core parser to make this work properly.

[brianhuffman]

Just now I was trying to do a proof involving Cryptol's toSignedInteger primitive (which is translated to sbvToInt in saw-core) by making it uninterpreted, and it doesn't work. Using the name "sbvToInt" or "Prelude.sbvToInt" with unint tactics seemingly has no effect.