Error: Uninterpreted constant used at incompatible types

[brianhuffman]

sawscript> let {{ p f g = (f 0x00 : [8]) == g 0x0 }}
sawscript> prove z3 {{ p }}
saw: Uninterpreted constant "|_|" used at incompatible types
      Current type      : SWord4 -> SWord8
      Previously used at: SWord8 -> SWord8
CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1037:23 in sbv-8.3-LGma1tAv1j88wp7VP3rPxf:Data.SBV.Core.Symbolic

When you use prove with a predicate that is not an explicit lambda, it invents names for the arguments, which all happen to be a single underscore "_". Then, since those arguments have function types, the proof backend turns them into uninterpreted functions. The problem is that the functions have the same name but different types, which causes the error in SBV.

If we use the same type for each, then SBV doesn't throw an error, but it does confuse the two arguments and the proof succeeds when it shouldn't:

sawscript> let {{ p f g = (f 0x00 : [8]) == g 0x00 }}
sawscript> prove z3 {{ p }}
[18:42:35.159] Valid

[brianhuffman]

I should also point out that this problem does not occur when you put an explicit lambda there instead of a defined constant. But then you run into issue #569 after the prover (rightly) finds a counterexample.

sawscript> prove z3 {{ \f g -> (f 0x00 : [8]) == g 0x00 }}
saw:
*** Data.SBV: Unexpected response from the solver, context: get-value:
***
***    Sent      : (get-value (|f|))
***    Expected  : a function value
***    Received  : ((|f| ((as const Array) #xff)))
***
***    Executable: z3
***    Options   : -nw -in -smt2

[brianhuffman]

Here's another variation: The prove command actually does the right thing if the predicate's arguments are ordinary bitvectors. (Although it is a bit confusing having both arguments named "_" in the counterexample.)

sawscript> let {{ p (a : [8]) (b : [4]) = drop a == b }}
sawscript> prove z3 {{ p }}
[18:51:43.044] prove: 1 unsolved subgoal(s)
[18:51:43.044] Invalid: [_ = 0, _ = 15]

But if the predicate's arguments are tuples, then we get the same error that we got above with function arguments.

sawscript> let {{ p (a:[2], b:[3]) (c, d) = (a, b) == (d, c) }}
sawscript> prove z3 {{ p }}
saw: Uninterpreted constant "|_.R|" used at incompatible types
      Current type      : SWord3
      Previously used at: SWord2
CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1037:23 in sbv-8.3-LGma1tAv1j88wp7VP3rPxf:Data.SBV.Core.Symbolic

This is surprising because first-order argument types should be translated as symbolic variables in SBV, not as uninterpreted functions.

[brianhuffman]

The what4 backend also has a similar problem. Here it appears that it is also trying to translate tuple-typed arguments as uninterpreted functions (which it shouldn't). Furthermore, producing an uninterpreted function fails when the name starts with an underscore.

sawscript> let {{ p (a:[2], b:[3]) (c, d) = (a, b) == (d, c) }}
sawscript> prove w4 {{ p }}

user error ("prove" (<stdin>:1:1-1:6):
"w4" (<stdin>:1:7-1:9):
Identifier must start with a letter.: Cannot create uninterpreted constant __L)