Some uninterpreted functions don't work with goal_eval_unint

[brianhuffman]

Some polymorphic function types can be made uninterpreted by commands like w4_unint_z3, but fail to work correctly with goal_eval_unint:

sawscript> prove do {w4_unint_z3 ["drop"]; } {{ \(x:[8]) x' -> x == x' ==> drop`{2} x == drop x' }}
[02:16:26.471] Valid
sawscript> prove do {goal_eval_unint ["drop"]; z3;} {{ \(x:[8]) x' -> x == x' ==> drop`{2} x == drop x' }}

Stack trace:
"prove" (<stdin>:1:1-1:6):
"goal_eval_unint" (<stdin>:1:11-1:26):
could not create uninterpreted function argument of type sort 0

The set of functions that can be made uninterpreted by either of these commands should be the same. goal_eval_unint should be extended to support the additional function types.

[RyanGlScott]

Despite this being closed, I'm still unable to run the original example in this issue using commit 988a026:

sawscript> prove do {w4_unint_z3 ["drop"]; } {{ \(x:[8]) x' -> x == x' ==> drop`{2} x == drop x' }}
[14:15:56.531] Valid
sawscript> prove do {goal_eval_unint ["drop"]; z3;} {{ \(x:[8]) x' -> x == x' ==> drop`{2} x == drop x' }}

Stack trace:
"prove" (<stdin>:1:1-1:6):
"goal_eval_unint" (<stdin>:1:11-1:26):
could not create uninterpreted function argument of type PrimName {primVarIndex = 133, primName = Prelude.Nat, primType = sort 0}

I originally ran into this in the context of trying to use goal_eval_unint ["join"], which produces a similar error message.

[brianhuffman]

My bad for not adding the example as a regression test in #1283. I just did a bisection and found that the regression was at commit 08c5995, which was part of PR #1191. That PR bumped the cryptol submodule to include GaloisInc/cryptol#1136, which made take and drop into cryptol primitives. (Previously they were both defined in terms of splitAt.) So it seems that the drop example in this thread is actually now an instance of #1044.

[RyanGlScott]

Ah, OK. In that case, I probably ran into #1044 as well when trying to use join in an uninterpreted way, as join is also a Cryptol primitive.

Should we close this issue in favor of #1044?

[brianhuffman]

Yeah, I think closing in favor of #1044 makes sense. We should make a reminder to add the example here to the regression test suite when #1044 is fixed.